1  /-
  2  Copyright (c) 2017 Johannes Hölzl. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot
  5  
  6  Theory of uniform spaces.
  7  
  8  Uniform spaces are a generalization of metric spaces and topological groups. Many concepts directly
  9  generalize to uniform spaces, e.g.
 10  
 11  * completeness
 12  * extension of uniform continuous functions to complete spaces
 13  * uniform contiunuity & embedding
 14  * totally bounded
 15  * totally bounded ∧ complete → compact
 16  
 17  The central concept of uniform spaces is its uniformity: a filter relating two elements of the
 18  space. This filter is reflexive, symmetric and transitive. So a set (i.e. a relation) in this filter
 19  represents a 'distance': it is reflexive, symmetric and the uniformity contains a set for which the
 20  `triangular` rule holds.
 21  
 22  The formalization is mostly based on the books:
 23    N. Bourbaki: General Topology
 24    I. M. James: Topologies and Uniformities
 25  A major difference is that this formalization is heavily based on the filter library.
 26  -/
 27  import order.filter.basic order.filter.lift topology.separation
src         └────────────────┘ └───────────────┘ └─────────────────┘
 28  
 29  open set lattice filter classical
 30  open_locale classical topological_space
 31  
 32  set_option eqn_compiler.zeta true
doc             └───────────────┘
 33  
 34  universes u
 35  section
 36  variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} {ι : Sort*}
 37  
 38  /-- The identity relation, or the graph of the identity function -/
 39  def id_rel {α : Type*} := {p : α × α | p.1 = p.2}
id                                         
src                                            
typ                                        
 40  
 41  @[simp] theorem mem_id_rel {a b : α} : (a, b) ∈ @id_rel α ↔ a = b := iff.rfl
id                                               └────┘         └─────┘
src                                                 └────┘            └─────┘
typ                                              └────┘         └─────┘
doc    └──┘                                           └────┘
 42  
 43  @[simp] theorem id_rel_subset {s : set (α × α)} : id_rel ⊆ s ↔ ∀ a, (a, a) ∈ s :=
id                                      └─┘         └────┘             
src                                     └─┘           └────┘                
typ                                     └─┘         └────┘             
doc    └──┘                                            └────┘
 44  by simp [subset_def]; exact forall_congr (λ a, by simp)
id            └────────┘         └──────────┘
src     └────┘└────────┘  └────┘└──────────┘  └──┘  └──┘└─
typ     └────┘└────────┘  └────┘└──────────┘  └──┘  └──┘└─
doc     └────┘            └────┘              └──┘  └──┘└─
txt     └────┘            └────┘              └──┘  └──┘└─
par     └────┘            └────┘              └──┘  └──┘└─
pid                                        └──┘  └────┘
st     └─────────────────────────────────────────────┘└───┘└─
 45  
src  
typ  
doc  
txt  
par  
pid  
st   
 46  /-- The composition of relations -/
 47  def comp_rel {α : Type u} (r₁ r₂ : set (α×α)) := {p : α × α | ∃z:α, (p.1, z) ∈ r₁ ∧ (z, p.2) ∈ r₂}
id                                      └─┘                          └┘        └┘
src                                     └─┘                                            
typ                                     └─┘                          └┘        └┘
 48  
 49  @[simp] theorem mem_comp_rel {r₁ r₂ : set (α×α)}
id                                         └─┘  
src                                        └─┘   
typ                                        └─┘  
doc    └──┘
 50    {x y : α} : (x, y) ∈ comp_rel r₁ r₂ ↔ ∃ z, (x, z) ∈ r₁ ∧ (z, y) ∈ r₂ := iff.rfl
id                     └──────┘ └┘ └┘         └┘       └┘    └─────┘
src                       └──────┘                                   └─────┘
typ                    └──────┘ └┘ └┘         └┘       └┘    └─────┘
doc                         └──────┘
 51  
 52  @[simp] theorem swap_id_rel : prod.swap '' id_rel = @id_rel α :=
id                                 └───────┘ └┘ └────┘   └────┘ 
src                                └───────┘ └┘ └────┘   └────┘
typ                                └───────┘ └┘ └────┘   └────┘ 
doc    └──┘                        └───────┘    └────┘    └────┘
 53  set.ext $ assume ⟨a, b⟩, by simp [image_swap_eq_preimage_swap]; exact eq_comm
id   └─────┘                          └─────────────────────────┘         └─────┘
src  └─────┘                     └────┘└─────────────────────────┘  └────┘└─────┘
typ  └─────┘                    └────┘└─────────────────────────┘  └────┘└─────┘
doc                              └────┘                             └────┘       
txt                              └────┘                             └────┘       
par                              └────┘                             └────┘       
pid                                                                           
st                              └──────────────────────────────────────────────────
 54  
src  
typ  
doc  
txt  
par  
pid  
st   
 55  theorem monotone_comp_rel [preorder β] {f g : β → set (α×α)}
id                              └──────┘             └─┘  
src                             └──────┘               └─┘   
typ                             └──────┘             └─┘  
 56    (hf : monotone f) (hg : monotone g) : monotone (λx, comp_rel (f x) (g x)) :=
id           └──────┘         └──────┘     └──────┘     └──────┘       
src          └──────┘          └──────┘      └──────┘      └──────┘
typ          └──────┘         └──────┘     └──────┘     └──────┘       
doc          └──────┘          └──────┘      └──────┘      └──────┘
 57  assume a b h p ⟨z, h₁, h₂⟩, ⟨z, hf h h₁, hg h h₂⟩
id                └┘  └┘       └┘      └┘ 
typ               └┘  └┘       └┘      └┘ 
 58  
 59  lemma prod_mk_mem_comp_rel {a b c : α} {s t : set (α×α)} (h₁ : (a, c) ∈ s) (h₂ : (c, b) ∈ t) :
id                                                └─┘                             
src                                                └─┘                                   
typ                                               └─┘                             
 60    (a, b) ∈ comp_rel s t :=
id          └──────┘  
src           └──────┘
typ         └──────┘  
doc             └──────┘
 61  ⟨c, h₁, h₂⟩
id      └┘  └┘
typ     └┘  └┘
 62  
 63  @[simp] lemma id_comp_rel {r : set (α×α)} : comp_rel id_rel r = r :=
id                                  └─┘       └──────┘ └────┘   
src                                 └─┘         └──────┘ └────┘   
typ                                 └─┘       └──────┘ └────┘   
doc    └──┘                                      └──────┘ └────┘
 64  set.ext $ assume ⟨a, b⟩, by simp
id   └─────┘          
src  └─────┘                     └────
typ  └─────┘                    └────
doc                              └────
txt                              └────
par                              └────
pid                                  
st                              └─────
 65  
src  
typ  
doc  
txt  
par  
pid  
st   
 66  lemma comp_rel_assoc {r s t : set (α×α)} :
id                                 └─┘  
src                                └─┘   
typ                                └─┘  
 67    comp_rel (comp_rel r s) t = comp_rel r (comp_rel s t) :=
id     └──────┘  └──────┘      └──────┘   └──────┘  
src    └──────┘  └──────┘         └──────┘    └──────┘
typ    └──────┘  └──────┘      └──────┘   └──────┘  
doc    └──────┘  └──────┘          └──────┘    └──────┘
 68  by ext p; cases p; simp only [mem_comp_rel]; tauto
id                                └──────────┘
src     └───┘  └────┘   └─────────┘└──────────┘  └─────
typ     └───┘  └────┘  └─────────┘└──────────┘  └─────
doc     └───┘  └────┘   └─────────┘              └─────
txt     └───┘  └────┘   └─────────┘              └─────
par     └───┘  └────┘   └─────────┘              └─────
pid        └┘              └──┘└┘                   
st     └────────────────────────────────────────────────
 69  
src  
typ  
doc  
txt  
par  
pid  
st   
 70  /-- This core description of a uniform space is outside of the type class hierarchy. It is useful
 71    for constructions of uniform spaces, when the topology is derived from the uniform space. -/
 72  structure uniform_space.core (α : Type u) :=
id                                     └──┘
typ                                    └──┘
 73  (uniformity : filter (α × α))
id                 └────┘    
src                └────┘    
typ                └────┘    
 74  (refl       : principal id_rel ≤ uniformity)
id                 └───────┘ └────┘  └────────┘
src                └───────┘ └────┘ 
typ                └───────┘ └────┘  └────────┘
doc                └───────┘ └────┘
 75  (symm       : tendsto prod.swap uniformity uniformity)
id                 └─────┘ └───────┘ └────────┘ └────────┘
src                └─────┘ └───────┘
typ                └─────┘ └───────┘ └────────┘ └────────┘
doc                └─────┘ └───────┘
 76  (comp       : uniformity.lift' (λs, comp_rel s s) ≤ uniformity)
id                 └────────┘└────┘     └──────┘     └────────┘
src                          └────┘      └──────┘      
typ                └────────┘└────┘     └──────┘     └────────┘
doc                          └────┘      └──────┘
 77  
 78  def uniform_space.core.mk' {α : Type u} (U : filter (α × α))
id                                                └────┘    
src                                               └────┘    
typ                                               └────┘    
 79    (refl : ∀ (r ∈ U) x, (x, x) ∈ r)
id                           
src                              
typ                          
 80    (symm : ∀ r ∈ U, {p | prod.swap p ∈ r} ∈ U)
id                       └───────┘      
src                         └───────┘       
typ                      └───────┘      
doc                          └───────┘
 81    (comp : ∀ r ∈ U, ∃ t ∈ U, comp_rel t t ⊆ r) : uniform_space.core α :=
id                         └──────┘        └────────────────┘ 
src                            └──────┘           └────────────────┘
typ                        └──────┘        └────────────────┘ 
doc                              └──────┘            └────────────────┘
 82  ⟨U, λ r ru, id_rel_subset.2 (refl _ ru), symm,
id         └┘  └───────────┘   └──┘   └┘   └──┘
src              └───────────┘   └──┘        └──┘
typ        └┘  └───────────┘   └──┘   └┘   └──┘
 83    begin
st     └─────
 84      intros r ru,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid            └───┘
st   ──────────────┘└─
 85      rw [mem_lift'_sets],
id           └────────────┘
src      └──┘└────────────┘
typ      └──┘└────────────┘
doc      └──┘              
txt      └──┘              
par      └──┘              
pid        └┘              
st   ─────────────────────┘└──
 86      exact comp _ ru,
id             └──┘   └┘
src      └────┘    └─┘
typ      └────┘└──┘└─┘└┘
doc      └────┘    └─┘
txt      └────┘    └─┘
par      └────┘    └─┘
pid               └─┘
st   ──────────────────┘└─
 87      apply monotone_comp_rel; exact monotone_id,
id             └───────────────┘        └─────────┘
src      └────┘└───────────────┘  └────┘└─────────┘
typ      └────┘└───────────────┘  └────┘└─────────┘
doc      └────┘                   └────┘
txt      └────┘                   └────┘
par      └────┘                   └────┘
pid                                   
st   ─────────────────────────────────────────────┘└─
 88    end⟩
st   ────┘
 89  
 90  /-- A uniform space generates a topological space -/
 91  def uniform_space.core.to_topological_space {α : Type u} (u : uniform_space.core α) :
id                                                                 └────────────────┘ 
src                                                                └────────────────┘
typ                                                                └────────────────┘ 
doc                                                                └────────────────┘
 92    topological_space α :=
id     └───────────────┘ 
src    └───────────────┘
typ    └───────────────┘ 
doc    └───────────────┘
 93  { is_open        := λs, ∀x∈s, { p : α × α | p.1 = x → p.2 ∈ s } ∈ u.uniformity,
id                                                     └─────────┘
src                                                              └─────────┘
typ                                                    └─────────┘
 94    is_open_univ   := by simp; intro; exact univ_mem_sets,
id                                             └───────────┘
src                         └──┘  └───┘  └────┘└───────────┘
typ                         └──┘  └───┘  └────┘└───────────┘
doc                         └──┘  └───┘  └────┘
txt                         └──┘  └───┘  └────┘
par                         └──┘  └───┘  └────┘
pid                                           
st                         └───────────────────────────────┘
 95    is_open_inter  :=
 96      assume s t hs ht x ⟨xs, xt⟩, by filter_upwards [hs x xs, ht x xt]; simp {contextual := tt},
id                └┘ └┘                              └┘  └┘  └┘  └┘                       └┘
src                                      └──────────────┘     └┘       └───┘ └────────────┘└┘
typ               └┘ └┘              └──────────────┘└┘└┘└┘└┘└┘  └───┘ └────────────┘└┘
doc                                      └──────────────┘     └┘       └───┘ └────────────┘  
txt                                      └──────────────┘     └┘       └───┘ └────────────┘  
par                                      └──────────────┘     └┘       └───┘ └────────────┘  
pid                                                    └┘     └┘            └────────────┘  
st                                      └─────────────────────────────────────────────────────────┘
 97    is_open_sUnion :=
 98      assume s hs x ⟨t, ts, xt⟩, by filter_upwards [hs t ts x xt] assume p ph h, ⟨t, ts, ph h⟩ }
id               └┘                                 └┘  └┘  └┘                    └┘
src                                    └──────────────┘        └┘      └───────┘  └┘  └┘   └┘
typ              └┘                 └──────────────┘└┘└┘└┘└┘      └───────┘ └┘└┘└┘   └┘
doc                                    └──────────────┘        └┘      └───────┘  └┘  └┘   └┘
txt                                    └──────────────┘        └┘      └───────┘  └┘  └┘   └┘
par                                    └──────────────┘        └┘      └───────┘  └┘  └┘   └┘
pid                                                  └┘              └───────┘  └┘  └┘   
st                                    └──────────────────────────────────────────────────────────┘
 99  
100  lemma uniform_space.core_eq : ∀{u₁ u₂ : uniform_space.core α}, u₁.uniformity = u₂.uniformity → u₁ = u₂
id                                          └────────────────┘    └┘└─────────┘  └┘└─────────┘   └┘  └┘
src                                          └────────────────┘       └─────────┘    └─────────┘      
typ                                         └────────────────┘    └┘└─────────┘  └┘└─────────┘   └┘  └┘
doc                                          └────────────────┘
101  | ⟨u₁, _, _, _⟩  ⟨u₂, _, _, _⟩ h := have u₁ = u₂, from h, by simp [*]
id      └┘             └┘                       
src                                                              └────────
typ     └┘             └┘                                       └────────
doc                                                               └────────
txt                                                               └────────
par                                                               └────────
pid                                                                   └─┘
st                                                               └─────────
102  
src  
typ  
doc  
txt  
par  
pid  
st   
103  section prio
104  set_option default_priority 100 -- see Note [default priority]
doc             └──────────────┘
105  /-- A uniform space is a generalization of the "uniform" topological aspects of a
106    metric space. It consists of a filter on `α × α` called the "uniformity", which
107    satisfies properties analogous to the reflexivity, symmetry, and triangle properties
108    of a metric.
109  
110    A metric space has a natural uniformity, and a uniform space has a natural topology.
111    A topological group also has a natural uniformity, even when it is not metrizable. -/
112  class uniform_space (α : Type u) extends topological_space α, uniform_space.core α :=
id                            └──┘            └───────────────┘   └────────────────┘ 
src                                           └───────────────┘    └────────────────┘
typ                           └──┘            └───────────────┘   └────────────────┘ 
doc                                           └───────────────┘    └────────────────┘
113  (is_open_uniformity : ∀s, is_open s ↔ (∀x∈s, { p : α × α | p.1 = x → p.2 ∈ s } ∈ uniformity))
id                            └─────┘                               └────────┘
src                            └─────┘                                       
typ                           └─────┘                               └────────┘
doc                            └─────┘
114  end prio
115  
116  @[pattern] def uniform_space.mk' {α} (t : topological_space α)
id                                             └───────────────┘ 
src                                            └───────────────┘
typ                                            └───────────────┘ 
doc    └─────┘                                 └───────────────┘
117    (c : uniform_space.core α)
id          └────────────────┘ 
src         └────────────────┘
typ         └────────────────┘ 
doc         └────────────────┘
118    (is_open_uniformity : ∀s:set α, t.is_open s ↔
id                              └─┘   └──────┘  
src                             └─┘     └──────┘   
typ                             └─┘   └──────┘  
119      (∀x∈s, { p : α × α | p.1 = x → p.2 ∈ s } ∈ c.uniformity)) :
id                                   └─────────┘
src                                           └─────────┘
typ                                  └─────────┘
120    uniform_space α := ⟨c, is_open_uniformity⟩
id     └───────────┘        └────────────────┘
src    └───────────┘
typ    └───────────┘        └────────────────┘
doc    └───────────┘
121  
122  def uniform_space.of_core {α : Type u} (u : uniform_space.core α) : uniform_space α :=
id                                               └────────────────┘     └───────────┘ 
src                                              └────────────────┘      └───────────┘
typ                                              └────────────────┘     └───────────┘ 
doc                                              └────────────────┘      └───────────┘
123  { to_core := u,
id                
typ               
124    to_topological_space := u.to_topological_space,
id                             └───────────────────┘
src                             └───────────────────┘
typ                            └───────────────────┘
doc                             └───────────────────┘
125    is_open_uniformity := assume a, iff.rfl }
id                                    └─────┘
src                                    └─────┘
typ                                   └─────┘
126  
127  def uniform_space.of_core_eq {α : Type u} (u : uniform_space.core α) (t : topological_space α)
id                                                  └────────────────┘        └───────────────┘ 
src                                                 └────────────────┘         └───────────────┘
typ                                                 └────────────────┘        └───────────────┘ 
doc                                                 └────────────────┘         └───────────────┘
128    (h : t = u.to_topological_space) : uniform_space α :=
id            └───────────────────┘    └───────────┘ 
src             └───────────────────┘    └───────────┘
typ           └───────────────────┘    └───────────┘ 
doc              └───────────────────┘    └───────────┘
129  { to_core := u,
id                
typ               
130    to_topological_space := t,
id                             
typ                            
131    is_open_uniformity := assume a, h.symm ▸ iff.rfl }
id                                    └───┘  └─────┘
src                                     └───┘  └─────┘
typ                                   └───┘  └─────┘
132  
133  lemma uniform_space.to_core_to_topological_space (u : uniform_space α) :
id                                                         └───────────┘ 
src                                                        └───────────┘
typ                                                        └───────────┘ 
doc                                                        └───────────┘
134    u.to_core.to_topological_space = u.to_topological_space :=
id     └──────┘└───────────────────┘  └───────────────────┘
src     └──────┘└───────────────────┘   └───────────────────┘
typ    └──────┘└───────────────────┘  └───────────────────┘
doc             └───────────────────┘
135  topological_space_eq $ funext $ assume s,
id   └──────────────────┘   └────┘          
src  └──────────────────┘   └────┘
typ  └──────────────────┘   └────┘          
136    by rw [uniform_space.core.to_topological_space, uniform_space.is_open_uniformity]
id            └─────────────────────────────────────┘  └──────────────────────────────┘
src       └──┘└─────────────────────────────────────┘└┘└──────────────────────────────┘└─
typ       └──┘└─────────────────────────────────────┘└┘└──────────────────────────────┘└─
doc       └──┘└─────────────────────────────────────┘└┘                                └─
txt       └──┘                                       └┘                                └─
par       └──┘                                       └┘                                └─
pid         └┘                                       └┘                                
st       └──────────────────────────────────────────┘└────────────────────────────────┘
137  
src  
typ  
doc  
txt  
par  
pid  
st   
138  @[ext]
doc    └─┘
139  lemma uniform_space_eq : ∀{u₁ u₂ : uniform_space α}, u₁.uniformity = u₂.uniformity → u₁ = u₂
id                                     └───────────┘    └┘└─────────┘  └┘└─────────┘   └┘  └┘
src                                     └───────────┘       └─────────┘    └─────────┘      
typ                                    └───────────┘    └┘└─────────┘  └┘└─────────┘   └┘  └┘
doc                                     └───────────┘
140  | (uniform_space.mk' t₁ u₁ o₁)  (uniform_space.mk' t₂ u₂ o₂) h :=
id                        └┘ └┘       └───────────────┘ └┘ └┘     
src                                   └───────────────┘
typ                       └┘ └┘       └───────────────┘ └┘ └┘     
141    have u₁ = u₂, from uniform_space.core_eq h,
id                       └───────────────────┘
src                      └───────────────────┘
typ                      └───────────────────┘
142    have t₁ = t₂, from topological_space_eq $ funext $ assume s, by rw [o₁, o₂]; simp [this],
id                       └──────────────────┘   └────┘                   └┘  └┘         └──┘
src                      └──────────────────┘   └────┘                └──┘  └┘    └────┘    
typ                      └──────────────────┘   └────┘               └──┘└┘└┘└┘  └────┘└──┘
doc                                                                    └──┘  └┘    └────┘    
txt                                                                    └──┘  └┘    └────┘    
par                                                                    └──┘  └┘    └────┘    
pid                                                                      └┘  └┘            
st                                                                    └─────┘└──┘└───────────┘
143    by simp [*]
src       └────────
typ       └────────
doc       └────────
txt       └────────
par       └────────
pid           └─┘
st       └─────────
144  
src  
typ  
doc  
txt  
par  
pid  
st   
145  lemma uniform_space.of_core_eq_to_core
146    (u : uniform_space α) (t : topological_space α) (h : t = u.to_core.to_topological_space) :
id          └───────────┘        └───────────────┘          └──────┘└───────────────────┘
src         └───────────┘         └───────────────┘             └──────┘└───────────────────┘
typ         └───────────┘        └───────────────┘          └──────┘└───────────────────┘
doc         └───────────┘         └───────────────┘                      └───────────────────┘
147    uniform_space.of_core_eq u.to_core t h = u :=
id     └──────────────────────┘ └──────┘    
src    └──────────────────────┘  └──────┘     
typ    └──────────────────────┘ └──────┘    
148  uniform_space_eq rfl
id   └──────────────┘ └─┘
src  └──────────────┘ └─┘
typ  └──────────────┘ └─┘
149  
150  section uniform_space
151  variables [uniform_space α]
id              └───────────┘
src             └───────────┘
typ             └───────────┘
doc             └───────────┘
152  
153  /-- The uniformity is a filter on α × α (inferred from an ambient uniform space
154    structure on α). -/
155  def uniformity (α : Type u) [uniform_space α] : filter (α × α) :=
id                                └───────────┘     └────┘    
src                               └───────────┘      └────┘    
typ                               └───────────┘     └────┘    
doc                               └───────────┘
156    (@uniform_space.to_core α _).uniformity
id       └───────────────────┘    └────────┘
src      └───────────────────┘     └────────┘
typ      └───────────────────┘    └────────┘
157  
158  localized "notation `𝓤` := uniformity" in uniformity
159  
160  lemma is_open_uniformity {s : set α} :
id                                 └─┘ 
src                                └─┘
typ                                └─┘ 
161    is_open s ↔ (∀x∈s, { p : α × α | p.1 = x → p.2 ∈ s } ∈ 𝓤 α) :=
id     └─────┘                                
src    └─────┘                                        
typ    └─────┘                                
doc    └─────┘                                                
162  uniform_space.is_open_uniformity s
id   └──────────────────────────────┘ 
src  └──────────────────────────────┘
typ  └──────────────────────────────┘ 
163  
164  lemma refl_le_uniformity : principal id_rel ≤ 𝓤 α :=
id                              └───────┘ └────┘   
src                             └───────┘ └────┘  
typ                             └───────┘ └────┘   
doc                             └───────┘ └────┘   
165  (@uniform_space.to_core α _).refl
id     └───────────────────┘    └──┘
src    └───────────────────┘     └──┘
typ    └───────────────────┘    └──┘
166  
167  lemma refl_mem_uniformity {x : α} {s : set (α × α)} (h : s ∈ 𝓤 α) :
id                                         └─┘               
src                                         └─┘                 
typ                                        └─┘               
doc                                                               
168    (x, x) ∈ s :=
id          
src          
typ         
169  refl_le_uniformity h rfl
id   └────────────────┘  └─┘
src  └────────────────┘   └─┘
typ  └────────────────┘  └─┘
170  
171  lemma symm_le_uniformity : map (@prod.swap α α) (𝓤 _) ≤ (𝓤 _) :=
id                              └─┘   └───────┘           
src                             └─┘   └───────┘             
typ                             └─┘   └───────┘           
doc                             └─┘   └───────┘              
172  (@uniform_space.to_core α _).symm
id     └───────────────────┘    └──┘
src    └───────────────────┘     └──┘
typ    └───────────────────┘    └──┘
173  
174  lemma comp_le_uniformity : (𝓤 α).lift' (λs:set (α×α), comp_rel s s) ≤ 𝓤 α :=
id                                 └───┘      └─┘     └──────┘      
src                                 └───┘      └─┘       └──────┘       
typ                                └───┘      └─┘     └──────┘      
doc                                 └───┘                 └──────┘        
175  (@uniform_space.to_core α _).comp
id     └───────────────────┘    └──┘
src    └───────────────────┘     └──┘
typ    └───────────────────┘    └──┘
176  
177  lemma tendsto_swap_uniformity : tendsto (@prod.swap α α) (𝓤 α) (𝓤 α) :=
id                                   └─────┘   └───────┘          
src                                  └─────┘   └───────┘            
typ                                  └─────┘   └───────┘          
doc                                  └─────┘   └───────┘            
178  symm_le_uniformity
id   └────────────────┘
src  └────────────────┘
typ  └────────────────┘
179  
180  lemma tendsto_const_uniformity {a : α} {f : filter β} : tendsto (λ _, (a, a)) f (𝓤 α) :=
id                                              └────┘     └─────┘              
src                                              └────┘      └─────┘                 
typ                                             └────┘     └─────┘              
doc                                                          └─────┘                  
181  assume s hs,
id           └┘
typ          └┘
182  show {x | (a, a) ∈ s} ∈ f,
id                   
src                     
typ                  
183    from univ_mem_sets' $ assume b, refl_mem_uniformity hs
id          └────────────┘            └─────────────────┘ └┘
src         └────────────┘             └─────────────────┘
typ         └────────────┘            └─────────────────┘ └┘
184  
185  lemma comp_mem_uniformity_sets {s : set (α × α)} (hs : s ∈ 𝓤 α) :
id                                       └─┘                
src                                      └─┘                  
typ                                      └─┘                
doc                                                             
186    ∃ t ∈ 𝓤 α, comp_rel t t ⊆ s :=
id           └──────┘    
src            └──────┘     
typ          └──────┘    
doc              └──────┘
187  have s ∈ (𝓤 α).lift' (λt:set (α×α), comp_rel t t),
id             └───┘      └─┘     └──────┘  
src              └───┘      └─┘       └──────┘
typ            └───┘      └─┘     └──────┘  
doc               └───┘                 └──────┘
188    from comp_le_uniformity hs,
id          └────────────────┘ └┘
src         └────────────────┘
typ         └────────────────┘ └┘
189  (mem_lift'_sets $ monotone_comp_rel monotone_id monotone_id).mp this
id    └────────────┘   └───────────────┘ └─────────┘ └─────────┘ └┘  └──┘
src   └────────────┘   └───────────────┘ └─────────┘ └─────────┘ └┘
typ   └────────────┘   └───────────────┘ └─────────┘ └─────────┘ └┘  └──┘
190  
191  lemma symm_of_uniformity {s : set (α × α)} (hs : s ∈ 𝓤 α) :
id                                 └─┘                
src                                └─┘                  
typ                                └─┘                
doc                                                       
192    ∃ t ∈ 𝓤 α, (∀a b, (a, b) ∈ t → (b, a) ∈ t) ∧ t ⊆ s :=
id                                  
src                                           
typ                                 
doc          
193  have preimage prod.swap s ∈ 𝓤 α, from symm_le_uniformity hs,
id        └──────┘ └───────┘           └────────────────┘ └┘
src       └──────┘ └───────┘             └────────────────┘
typ       └──────┘ └───────┘           └────────────────┘ └┘
doc       └──────┘ └───────┘     
194  ⟨s ∩ preimage prod.swap s, inter_mem_sets hs this, assume a b ⟨h₁, h₂⟩, ⟨h₂, h₁⟩, inter_subset_left _ _⟩
id      └──────┘ └───────┘   └────────────┘ └┘ └──┘           └┘  └┘             └───────────────┘
src      └──────┘ └───────┘    └────────────┘                                         └───────────────┘
typ     └──────┘ └───────┘   └────────────┘ └┘ └──┘           └┘  └┘             └───────────────┘
doc       └──────┘ └───────┘
195  
196  lemma comp_symm_of_uniformity {s : set (α × α)} (hs : s ∈ 𝓤 α) :
id                                      └─┘                
src                                     └─┘                  
typ                                     └─┘                
doc                                                            
197    ∃ t ∈ 𝓤 α, (∀{a b}, (a, b) ∈ t → (b, a) ∈ t) ∧ comp_rel t t ⊆ s :=
id                                  └──────┘    
src                                           └──────┘     
typ                                 └──────┘    
doc                                                  └──────┘
198  let ⟨t, ht₁, ht₂⟩ := comp_mem_uniformity_sets hs in
id   └─┘     └─┘  └─┘     └──────────────────────┘ └┘
src                       └──────────────────────┘
typ  └─┘     └─┘  └─┘     └──────────────────────┘ └┘
199  let ⟨t', ht', ht'₁, ht'₂⟩ := symm_of_uniformity ht₁ in
id   └─┘  └┘  └─┘  └──┘  └──┘     └────────────────┘
src                               └────────────────┘
typ  └─┘  └┘  └─┘  └──┘  └──┘     └────────────────┘
200  ⟨t', ht', ht'₁, subset.trans (monotone_comp_rel monotone_id monotone_id ht'₂) ht₂⟩
id                   └──────────┘  └───────────────┘ └─────────┘ └─────────┘
src                  └──────────┘  └───────────────┘ └─────────┘ └─────────┘
typ                  └──────────┘  └───────────────┘ └─────────┘ └─────────┘
201  
202  lemma uniformity_le_symm : 𝓤 α ≤ (@prod.swap α α) <$> 𝓤 α :=
id                                   └───────┘    └─┘  
src                                   └───────┘      └─┘ 
typ                                  └───────┘    └─┘  
doc                                    └───────┘          
203  by rw [map_swap_eq_comap_swap];
id          └────────────────────┘
src     └──┘└────────────────────┘
typ     └──┘└────────────────────┘
doc     └──┘                      
txt     └──┘                      
par     └──┘                      
pid       └┘                      
st     └─────────────────────────┘└─
204  from map_le_iff_le_comap.1 tendsto_swap_uniformity
id        └─────────────────┘   └─────────────────────┘
src  └───┘└─────────────────┘└─┘└─────────────────────┘
typ  └───┘└─────────────────┘└─┘└─────────────────────┘
doc  └───┘                   └─┘                       
txt  └───┘                   └─┘                       
par  └───┘                   └─┘                       
pid  └───┘                   └─┘                       
st   ───────────────────────────────────────────────────
205  
src  
typ  
doc  
txt  
par  
pid  
st   
206  lemma uniformity_eq_symm : 𝓤 α = (@prod.swap α α) <$> 𝓤 α :=
id                                   └───────┘    └─┘  
src                                   └───────┘      └─┘ 
typ                                  └───────┘    └─┘  
doc                                    └───────┘          
207  le_antisymm uniformity_le_symm symm_le_uniformity
id   └─────────┘ └────────────────┘ └────────────────┘
src  └─────────┘ └────────────────┘ └────────────────┘
typ  └─────────┘ └────────────────┘ └────────────────┘
208  
209  theorem uniformity_lift_le_swap {g : set (α×α) → filter β} {f : filter β} (hg : monotone g)
id                                        └─┘      └────┘        └────┘         └──────┘ 
src                                       └─┘        └────┘         └────┘          └──────┘
typ                                       └─┘      └────┘        └────┘         └──────┘ 
doc                                                                                  └──────┘
210    (h : (𝓤 α).lift (λs, g (preimage prod.swap s)) ≤ f) : (𝓤 α).lift g ≤ f :=
id             └──┘        └──────┘ └───────┘            └──┘    
src             └──┘          └──────┘ └───────┘               └──┘    
typ            └──┘        └──────┘ └───────┘            └──┘    
doc             └──┘          └──────┘ └───────┘                └──┘
211  calc (𝓤 α).lift g ≤ (filter.map (@prod.swap α α) $ 𝓤 α).lift g :
id           └──┘      └────────┘   └───────┘        └──┘  
src           └──┘       └────────┘   └───────┘           └──┘
typ          └──┘      └────────┘   └───────┘        └──┘  
doc           └──┘       └────────┘   └───────┘           └──┘
212      lift_mono uniformity_le_symm (le_refl _)
id       └───────┘ └────────────────┘  └─────┘
src      └───────┘ └────────────────┘  └─────┘
typ      └───────┘ └────────────────┘  └─────┘
213    ... ≤ _ :
214      by rw [map_lift_eq2 hg, image_swap_eq_preimage_swap]; exact h
id              └──────────┘ └┘  └─────────────────────────┘         
src         └──┘└──────────┘  └┘└─────────────────────────┘  └────┘ 
typ         └──┘└──────────┘└┘└┘└─────────────────────────┘  └────┘
doc         └──┘              └┘                             └────┘ 
txt         └──┘              └┘                             └────┘ 
par         └──┘              └┘                             └────┘ 
pid           └┘              └┘                                   
st         └──────────────────┘└───────────────────────────┘└─────────
215  
src  
typ  
doc  
txt  
par  
pid  
st   
216  lemma uniformity_lift_le_comp {f : set (α×α) → filter β} (h : monotone f) :
id                                      └─┘      └────┘        └──────┘ 
src                                     └─┘        └────┘         └──────┘
typ                                     └─┘      └────┘        └──────┘ 
doc                                                                └──────┘
217    (𝓤 α).lift (λs, f (comp_rel s s)) ≤ (𝓤 α).lift f :=
id        └──┘        └──────┘         └──┘  
src        └──┘          └──────┘            └──┘
typ       └──┘        └──────┘         └──┘  
doc        └──┘          └──────┘             └──┘
218  calc (𝓤 α).lift (λs, f (comp_rel s s)) =
id           └──┘        └──────┘  
src           └──┘          └──────┘
typ          └──┘        └──────┘  
doc           └──┘          └──────┘
219      ((𝓤 α).lift' (λs:set (α×α), comp_rel s s)).lift f :
id           └───┘      └─┘     └──────┘    └──┘  
src           └───┘      └─┘       └──────┘      └──┘
typ          └───┘      └─┘     └──────┘    └──┘  
doc           └───┘                 └──────┘      └──┘
220    begin
st     └─────
221      rw [lift_lift'_assoc],
id           └──────────────┘
src      └──┘└──────────────┘
typ      └──┘└──────────────┘
doc      └──┘                
txt      └──┘                
par      └──┘                
pid        └┘                
st   ───────────────────────┘└──
222      exact monotone_comp_rel monotone_id monotone_id,
id             └───────────────┘             └─────────┘
src      └────┘└───────────────┘           └─────────┘
typ      └────┘└───────────────┘           └─────────┘
doc      └────┘                            
txt      └────┘                            
par      └────┘                            
pid                                       
st   ──────────────────────────────────────────────────┘└─
223      exact h
id             
src      └────┘ 
typ      └────┘
doc      └────┘ 
txt      └────┘ 
par      └────┘ 
pid            
st   ────────────
224    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
225    ... ≤ (𝓤 α).lift f : lift_mono comp_le_uniformity (le_refl _)
id              └──┘     └───────┘ └────────────────┘  └─────┘
src              └──┘      └───────┘ └────────────────┘  └─────┘
typ             └──┘     └───────┘ └────────────────┘  └─────┘
doc              └──┘
226  
227  lemma comp_le_uniformity3 :
228    (𝓤 α).lift' (λs:set (α×α), comp_rel s (comp_rel s s)) ≤ (𝓤 α) :=
id        └───┘      └─┘     └──────┘   └──────┘        
src        └───┘      └─┘       └──────┘    └──────┘         
typ       └───┘      └─┘     └──────┘   └──────┘        
doc        └───┘                 └──────┘    └──────┘          
229  calc (𝓤 α).lift' (λd, comp_rel d (comp_rel d d)) =
id           └───┘      └──────┘   └──────┘  
src           └───┘       └──────┘    └──────┘
typ          └───┘      └──────┘   └──────┘  
doc           └───┘       └──────┘    └──────┘
230    (𝓤 α).lift (λs, (𝓤 α).lift' (λt:set(α×α), comp_rel s (comp_rel t t))) :
id        └──┘         └───┘      └─┘    └──────┘   └──────┘  
src        └──┘           └───┘      └─┘      └──────┘    └──────┘
typ       └──┘         └───┘      └─┘    └──────┘   └──────┘  
doc        └──┘           └───┘                └──────┘    └──────┘
231    begin
st     └─────
232      rw [lift_lift'_same_eq_lift'],
id           └──────────────────────┘
src      └──┘└──────────────────────┘
typ      └──┘└──────────────────────┘
doc      └──┘                        
txt      └──┘                        
par      └──┘                        
pid        └┘                        
st   ───────────────────────────────┘└──
233      exact (assume x, monotone_comp_rel monotone_const $ monotone_comp_rel monotone_id monotone_id),
id                                          └────────────┘   └───────────────┘             └─────────┘
src      └────┘       └──┘                 └────────────┘ └───────────────┘           └─────────┘
typ      └────┘       └──┘                 └────────────┘ └───────────────┘           └─────────┘
doc      └────┘       └──┘                                                                       
txt      └────┘       └──┘                                                                       
par      └────┘       └──┘                                                                       
pid                  └──┘                                                                       
st   ─────────────────────────────────────────────────────────────────────────────────────────────────┘└─
234      exact (assume x, monotone_comp_rel monotone_id monotone_const),
id                        └───────────────┘ └─────────┘ └────────────┘
src      └────┘       └──┘└───────────────┘└─────────┘└────────────┘
typ      └────┘       └──┘└───────────────┘└─────────┘└────────────┘
doc      └────┘       └──┘                                          
txt      └────┘       └──┘                                          
par      └────┘       └──┘                                          
pid                  └──┘                                          
st   ─────────────────────────────────────────────────────────────────┘└─
235    end
st   ────┘
236    ... ≤ (𝓤 α).lift (λs, (𝓤 α).lift' (λt:set(α×α), comp_rel s t)) :
id              └──┘         └───┘      └─┘    └──────┘  
src              └──┘           └───┘      └─┘      └──────┘
typ             └──┘         └───┘      └─┘    └──────┘  
doc              └──┘           └───┘                └──────┘
237      lift_mono' $ assume s hs, @uniformity_lift_le_comp α _ _ (principal ∘ comp_rel s) $
id       └────────┘           └┘   └─────────────────────┘       └───────┘  └──────┘ 
src      └────────┘                 └─────────────────────┘        └───────┘  └──────┘
typ      └────────┘           └┘   └─────────────────────┘       └───────┘  └──────┘ 
doc                                                                └───────┘   └──────┘
238        monotone_principal.comp (monotone_comp_rel monotone_const monotone_id)
id         └────────────────┘└───┘  └───────────────┘ └────────────┘ └─────────┘
src        └────────────────┘└───┘  └───────────────┘ └────────────┘ └─────────┘
typ        └────────────────┘└───┘  └───────────────┘ └────────────┘ └─────────┘
239    ... = (𝓤 α).lift' (λs:set(α×α), comp_rel s s) :
id              └───┘      └─┘    └──────┘  
src              └───┘      └─┘      └──────┘
typ             └───┘      └─┘    └──────┘  
doc              └───┘                └──────┘
240      lift_lift'_same_eq_lift'
id       └──────────────────────┘
src      └──────────────────────┘
typ      └──────────────────────┘
241        (assume s, monotone_comp_rel monotone_const monotone_id)
id                   └───────────────┘ └────────────┘ └─────────┘
src                   └───────────────┘ └────────────┘ └─────────┘
typ                  └───────────────┘ └────────────┘ └─────────┘
242        (assume s, monotone_comp_rel monotone_id monotone_const)
id                   └───────────────┘ └─────────┘ └────────────┘
src                   └───────────────┘ └─────────┘ └────────────┘
typ                  └───────────────┘ └─────────┘ └────────────┘
243    ... ≤ (𝓤 α) : comp_le_uniformity
id                 └────────────────┘
src                 └────────────────┘
typ                └────────────────┘
doc           
244  
245  lemma mem_nhds_uniformity_iff {x : α} {s : set α} :
id                                             └─┘ 
src                                             └─┘
typ                                            └─┘ 
246    s ∈ 𝓝 x ↔ {p : α × α | p.1 = x → p.2 ∈ s} ∈ 𝓤 α :=
id                                
src                                      
typ                               
doc                                               
247  ⟨ begin
st     └─────
248      simp only [mem_nhds_sets_iff, is_open_uniformity, and_imp, exists_imp_distrib],
id                  └───────────────┘  └────────────────┘  └─────┘  └────────────────┘
src      └─────────┘└───────────────┘└┘└────────────────┘└┘└─────┘└┘└────────────────┘
typ      └─────────┘└───────────────┘└┘└────────────────┘└┘└─────┘└┘└────────────────┘
doc      └─────────┘                 └┘                  └┘       └┘                  
txt      └─────────┘                 └┘                  └┘       └┘                  
par      └─────────┘                 └┘                  └┘       └┘                  
pid          └──┘└┘                 └┘                  └┘       └┘                  
st   ─────────────────────────────────────────────────────────────────────────────────┘└─
249      exact assume t ts ht xt, by filter_upwards [ht x xt] assume ⟨x', y⟩ h eq, ts $ h eq
id                                                   └┘  └┘                       └┘
src      └────┘      └───────────┘  └──────────────┘     └┘      └┘  └┘ └──────┘      
typ      └────┘      └───────────┘  └──────────────┘└┘└┘└┘      └┘  └┘ └──────┘└┘    
doc      └────┘      └───────────┘  └──────────────┘     └┘      └┘  └┘ └──────┘      
txt      └────┘      └───────────┘  └──────────────┘     └┘      └┘  └┘ └──────┘      
par      └────┘      └───────────┘  └──────────────┘     └┘      └┘  └┘ └──────┘      
pid                 └───────────┘  └───────────────┘     └┘      └┘  └┘ └──────┘      
st   ──────────────────────────────┘└────────────────────────────────────────────────────────
250    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
251  
252    assume hs,
id            └┘
typ           └┘
253    mem_nhds_sets_iff.mpr ⟨{x | {p : α × α | p.1 = x → p.2 ∈ s} ∈ 𝓤 α},
id     └───────────────┘└──┘                           
src    └───────────────┘└──┘                                 
typ    └───────────────┘└──┘                           
doc                                                                  
254      assume x' hx', refl_mem_uniformity hx' rfl,
id              └┘ └─┘  └─────────────────┘ └─┘ └─┘
src                     └─────────────────┘     └─┘
typ             └┘ └─┘  └─────────────────┘ └─┘ └─┘
255      is_open_uniformity.mpr $ assume x' hx',
id       └────────────────┘└──┘          └┘ └─┘
src      └────────────────┘└──┘
typ      └────────────────┘└──┘          └┘ └─┘
256        let ⟨t, ht, tr⟩ := comp_mem_uniformity_sets hx' in
id         └─┘                └──────────────────────┘ └─┘
src                           └──────────────────────┘
typ        └─┘                └──────────────────────┘ └─┘
257        by filter_upwards [ht] assume ⟨a, b⟩ hp' (hax' : a = x'),
id                                                            └┘
src           └──────────────┘  └┘      └┘ └┘ └────────────┘   └──
typ           └──────────────┘  └┘      └┘└┘ └────────────┘ └┘└──
doc           └──────────────┘  └┘      └┘ └┘ └────────────┘    └──
txt           └──────────────┘  └┘      └┘ └┘ └────────────┘    └──
par           └──────────────┘  └┘      └┘ └┘ └────────────┘    └──
pid                         └┘        └┘ └┘ └────────────┘    └──
st           └───────────────────────────────────────────────────────
258        by filter_upwards [ht] assume ⟨a, b'⟩ hp'' (hab : a = b),
id                                          └┘                
src  ─────┘  └───────────────┘  └┘      └┘ └┘  └────────────┘   └──
typ  ─────┘  └───────────────┘  └┘      └┘└┘└┘└────────────┘  └──
doc  ─────┘  └───────────────┘  └┘      └┘ └┘  └────────────┘   └──
txt  ─────┘  └───────────────┘  └┘      └┘ └┘  └────────────┘   └──
par  ─────┘  └───────────────┘  └┘      └┘ └┘  └────────────┘   └──
pid  ─────┘  └───────────────┘  └┘      └┘ └┘  └────────────┘   └──
st   ───────┘└───────────────────────────────────────────────────────
259        have hp : (x', b) ∈ t, from hax' ▸ hp',
id                                   └──┘   └─┘
src  ─────┘    └────┘  └┘ └┘ └─────┘        └─
typ  ─────┘    └────┘  └┘ └┘ └─────┘└──┘ └─┘└─
doc  ─────┘    └────┘   └┘ └┘  └─────┘        └─
txt  ─────┘    └────┘   └┘ └┘  └─────┘        └─
par  ─────┘    └────┘   └┘ └┘  └─────┘        └─
pid  ─────┘    └────┘   └┘ └┘  └─────┘        └─
st   ──────────────────────────────────────────────
260        have (b, b') ∈ t, from hab ▸ hp'',
id                                    
src  ─────┘      └┘  └┘  └─────┘       └─
typ  ─────┘      └┘  └┘  └─────┘       └─
doc  ─────┘      └┘  └┘  └─────┘        └─
txt  ─────┘      └┘  └┘  └─────┘        └─
par  ─────┘      └┘  └┘  └─────┘        └─
pid  ─────┘      └┘  └┘  └─────┘        └─
st   ─────────────────────────────────────────
261        have (x', b') ∈ comp_rel t t, from ⟨b, hp, this⟩,
id               └┘        └──────┘           
src  ─────┘       └┘  └┘ └──────┘  └─────┘  └┘  └┘    └──
typ  ─────┘     └┘└┘  └┘ └──────┘ └─────┘ └┘  └┘    └──
doc  ─────┘       └┘  └┘ └──────┘  └─────┘  └┘  └┘    └──
txt  ─────┘       └┘  └┘           └─────┘  └┘  └┘    └──
par  ─────┘       └┘  └┘           └─────┘  └┘  └┘    └──
pid  ─────┘       └┘  └┘           └─────┘  └┘  └┘    └──
st   ────────────────────────────────────────────────────────
262        show b' ∈ s,
id                  
src  ─────┘        └─
typ  ─────┘      └─
doc  ─────┘        └─
txt  ─────┘        └─
par  ─────┘        └─
pid  ─────┘        └─
st   ───────────────────
263          from tr this rfl,
id                └┘      └─┘
src  ────────────┘      └─┘
typ  ────────────┘└┘    └─┘
doc  ────────────┘      
txt  ────────────┘      
par  ────────────┘      
pid  ────────────┘      
st   ───────────────────────┘
264      hs⟩⟩
id       └┘
typ      └┘
265  
266  lemma nhds_eq_comap_uniformity {x : α} : 𝓝 x = (𝓤 α).comap (prod.mk x) :=
id                                                 └───┘   └─────┘ 
src                                                   └───┘   └─────┘
typ                                                └───┘   └─────┘ 
doc                                                    └───┘
267  by ext s; rw [mem_nhds_uniformity_iff, mem_comap_sets]; from iff.intro
id                 └─────────────────────┘  └────────────┘        └───────┘
src     └───┘  └──┘└─────────────────────┘└┘└────────────┘  └───┘└───────┘
typ     └───┘  └──┘└─────────────────────┘└┘└────────────┘  └───┘└───────┘
doc     └───┘  └──┘                       └┘                └───┘         
txt     └───┘  └──┘                       └┘                └───┘         
par     └───┘  └──┘                       └┘                └───┘         
pid        └┘    └┘                       └┘                └───┘         
st     └──────────┘└─────────────────────┘└──────────────┘└────────────────
268    (assume hs, ⟨_, hs, assume x hx, hx rfl⟩)
id                                         └─┘
src  ─┘       └───┘ └─┘  └┘      └─────┘  └─┘└──
typ  ─┘       └───┘ └─┘  └┘      └─────┘  └─┘└──
doc  ─┘       └───┘ └─┘  └┘      └─────┘     └──
txt  ─┘       └───┘ └─┘  └┘      └─────┘     └──
par  ─┘       └───┘ └─┘  └┘      └─────┘     └──
pid  ─┘       └───┘ └─┘  └┘      └─────┘     └──
st   ────────────────────────────────────────────
269    (assume ⟨t, h, ht⟩, (𝓤 α).sets_of_superset h $
id                   └┘     
src  ─┘       └┘ └┘ └┘  └─┘  └─────────────────┘  
typ  ─┘       └┘ └┘└┘└┘└─┘ └─────────────────┘  
doc  ─┘       └┘ └┘ └┘  └─┘  └─────────────────┘  
txt  ─┘       └┘ └┘ └┘  └─┘   └─────────────────┘  
par  ─┘       └┘ └┘ └┘  └─┘   └─────────────────┘  
pid  ─┘       └┘ └┘ └┘  └─┘   └─────────────────┘  
st   ─────────────────────────────────────────────────
270      assume ⟨p₁, p₂⟩ hp (h : p₁ = x), ht $ by simp [h.symm, hp])
id               └┘                                           └┘
src  ───┘      └┘  └┘  └────────┘   └─┘     └────┘      └┘  └─
typ  ───┘      └┘└┘└┘  └────────┘  └─┘     └────┘└────┘└┘└┘└─
doc  ───┘      └┘  └┘  └────────┘    └─┘     └────┘      └┘  └─
txt  ───┘      └┘  └┘  └────────┘    └─┘     └────┘      └┘  └─
par  ───┘      └┘  └┘  └────────┘    └─┘     └────┘      └┘  └─
pid  ───┘      └┘  └┘  └────────┘    └─┘     └─────┘      └┘  └┘
st   ───────────────────────────────────────────┘└────────────────┘└─
271  
src  
typ  
doc  
txt  
par  
pid  
st   
272  lemma nhds_eq_uniformity {x : α} : 𝓝 x = (𝓤 α).lift' (λs:set (α×α), {y | (x, y) ∈ s}) :=
id                                           └───┘      └─┘             
src                                             └───┘      └─┘                 
typ                                          └───┘      └─┘             
doc                                              └───┘
273  begin
st   └─────
274    ext s,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid       └┘
st   ──────┘└─
275    rw [mem_lift'_sets], tactic.swap, apply monotone_preimage,
id         └────────────┘   └─────────┘        └───────────────┘
src    └──┘└────────────┘  └─────────┘  └────┘└───────────────┘
typ    └──┘└────────────┘  └─────────┘  └────┘└───────────────┘
doc    └──┘                └─────────┘  └────┘
txt    └──┘                             └────┘
par    └──┘                └─────────┘  └────┘
pid      └┘                                  
st   ───────────────────┘└────────────┘└───────────────────────┘└─
276    simp [mem_nhds_uniformity_iff],
id           └─────────────────────┘
src    └────┘└─────────────────────┘
typ    └────┘└─────────────────────┘
doc    └────┘                       
txt    └────┘                       
par    └────┘                       
pid                               
st   ───────────────────────────────┘└─
277    exact ⟨assume h, ⟨_, h, assume y h, h rfl⟩,
id                                           └─┘
src    └────┘       └──┘ └─┘ └┘      └────┘ └─┘└──
typ    └────┘       └──┘ └─┘ └┘      └────┘ └─┘└──
doc    └────┘       └──┘ └─┘ └┘      └────┘    └──
txt    └────┘       └──┘ └─┘ └┘      └────┘    └──
par    └────┘       └──┘ └─┘ └┘      └────┘    └──
pid                └──┘ └─┘ └┘      └────┘    └──
st   ──────────────────────────────────────────────
278      assume ⟨t, h₁, h₂⟩,
id                 └┘  └┘
src  ───┘      └┘ └┘  └┘  └──
typ  ───┘      └┘└┘└┘└┘└┘└──
doc  ───┘      └┘ └┘  └┘  └──
txt  ───┘      └┘ └┘  └┘  └──
par  ───┘      └┘ └┘  └┘  └──
pid  ───┘      └┘ └┘  └┘  └──
st   ────────────────────────
279      (𝓤 α).sets_of_superset h₁ $
id         
src  ───┘  └─────────────────┘   
typ  ───┘ └─────────────────┘   
doc  ───┘  └─────────────────┘   
txt  ───┘   └─────────────────┘   
par  ───┘   └─────────────────┘   
pid  ───┘   └─────────────────┘   
st   ────────────────────────────────
280      assume ⟨x', y⟩ hp (eq : x' = x), h₂ $
id               └┘                
src  ───┘      └┘  └┘ └─────────┘   └─┘   
typ  ───┘      └┘└┘└┘└─────────┘   └─┘   
doc  ───┘      └┘  └┘ └─────────┘    └─┘   
txt  ───┘      └┘  └┘ └─────────┘    └─┘   
par  ───┘      └┘  └┘ └─────────┘    └─┘   
pid  ───┘      └┘  └┘ └─────────┘    └─┘   
st   ──────────────────────────────────────────
281      show (x, y) ∈ t, from eq ▸ hp⟩
id                              
src  ───┘      └┘ └┘ └─────┘    └┘
typ  ───┘     └┘ └┘ └─────┘    └┘
doc  ───┘      └┘ └┘  └─────┘     └┘
txt  ───┘      └┘ └┘  └─────┘     └┘
par  ───┘      └┘ └┘  └─────┘     └┘
pid  ───┘      └┘ └┘  └─────┘     
st   ──────────────────────────────────┘
282  end
st   └─┘
283  
284  lemma mem_nhds_left (x : α) {s : set (α×α)} (h : s ∈ 𝓤 α) :
id                                   └─┘             
src                                   └─┘               
typ                                  └─┘             
doc                                                       
285    {y : α | (x, y) ∈ s} ∈ 𝓝 x :=
id                     
src                       
typ                    
doc                           
286  have 𝓝 x ≤ principal {y : α | (x, y) ∈ s},
id           └───────┘             
src           └───────┘               
typ          └───────┘             
doc            └───────┘
287    by rw [nhds_eq_uniformity]; exact infi_le_of_le s (infi_le _ h),
id            └────────────────┘         └───────────┘   └─────┘   
src       └──┘└────────────────┘  └────┘└───────────┘  └─────┘└─┘ 
typ       └──┘└────────────────┘  └────┘└───────────┘ └─────┘└─┘
doc       └──┘                    └────┘                      └─┘ 
txt       └──┘                    └────┘                      └─┘ 
par       └──┘                    └────┘                      └─┘ 
pid         └┘                                               └─┘ 
st       └─────────────────────┘└───────────────────────────────────┘
288  by simp at this; assumption
src     └──────────┘  └──────────
typ     └──────────┘  └──────────
doc     └──────────┘  └──────────
txt     └──────────┘  └──────────
par     └──────────┘  └──────────
pid         └─────┘            
st     └─────────────────────────
289  
src  
typ  
doc  
txt  
par  
pid  
st   
290  lemma mem_nhds_right (y : α) {s : set (α×α)} (h : s ∈ 𝓤 α) :
id                                    └─┘             
src                                    └─┘               
typ                                   └─┘             
doc                                                        
291    {x : α | (x, y) ∈ s} ∈ 𝓝 y :=
id                     
src                       
typ                    
doc                           
292  mem_nhds_left _ (symm_le_uniformity h)
id   └───────────┘    └────────────────┘ 
src  └───────────┘    └────────────────┘
typ  └───────────┘    └────────────────┘ 
293  
294  lemma tendsto_right_nhds_uniformity {a : α} : tendsto (λa', (a', a)) (𝓝 a) (𝓤 α) :=
id                                                └─────┘   └┘  └┘           
src                                                └─────┘                     
typ                                               └─────┘   └┘  └┘           
doc                                                └─────┘                      
295  assume s, mem_nhds_right a
id            └────────────┘ 
src            └────────────┘
typ           └────────────┘ 
296  
297  lemma tendsto_left_nhds_uniformity {a : α} : tendsto (λa', (a, a')) (𝓝 a) (𝓤 α) :=
id                                               └─────┘   └┘    └┘         
src                                               └─────┘                     
typ                                              └─────┘   └┘    └┘         
doc                                               └─────┘                      
298  assume s, mem_nhds_left a
id            └───────────┘ 
src            └───────────┘
typ           └───────────┘ 
299  
300  lemma lift_nhds_left {x : α} {g : set α → filter β} (hg : monotone g) :
id                                    └─┘    └────┘         └──────┘ 
src                                    └─┘     └────┘          └──────┘
typ                                   └─┘    └────┘         └──────┘ 
doc                                                            └──────┘
301    (𝓝 x).lift g = (𝓤 α).lift (λs:set (α×α), g {y | (x, y) ∈ s}) :=
id        └──┘       └──┘      └─┘              
src        └──┘         └──┘      └─┘                   
typ       └──┘       └──┘      └─┘              
doc        └──┘          └──┘
302  eq.trans
id   └──────┘
src  └──────┘
typ  └──────┘
303    begin
st     └─────
304      rw [nhds_eq_uniformity],
id           └────────────────┘
src      └──┘└────────────────┘
typ      └──┘└────────────────┘
doc      └──┘                  
txt      └──┘                  
par      └──┘                  
pid        └┘                  
st   ─────────────────────────┘└──
305      exact (filter.lift_assoc $ monotone_principal.comp $ monotone_preimage.comp monotone_preimage )
id              └───────────────┘   └─────────────────────┘   └────────────────────┘ └───────────────┘
src      └────┘ └───────────────┘ └─────────────────────┘ └────────────────────┘└───────────────┘└──
typ      └────┘ └───────────────┘ └─────────────────────┘ └────────────────────┘└───────────────┘└──
doc      └────┘                                                                                  └──
txt      └────┘                                                                                  └──
par      └────┘                                                                                  └──
pid                                                                                             └┘
st   ────────────────────────────────────────────────────────────────────────────────────────────────────
306    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
307    (congr_arg _ $ funext $ assume s, filter.lift_principal hg)
id      └───────┘     └────┘            └───────────────────┘ └┘
src     └───────┘     └────┘             └───────────────────┘
typ     └───────┘     └────┘            └───────────────────┘ └┘
308  
309  lemma lift_nhds_right {x : α} {g : set α → filter β} (hg : monotone g) :
id                                     └─┘    └────┘         └──────┘ 
src                                     └─┘     └────┘          └──────┘
typ                                    └─┘    └────┘         └──────┘ 
doc                                                             └──────┘
310    (𝓝 x).lift g = (𝓤 α).lift (λs:set (α×α), g {y | (y, x) ∈ s}) :=
id        └──┘       └──┘      └─┘              
src        └──┘         └──┘      └─┘                   
typ       └──┘       └──┘      └─┘              
doc        └──┘          └──┘
311  calc (𝓝 x).lift g = (𝓤 α).lift (λs:set (α×α), g {y | (x, y) ∈ s}) : lift_nhds_left hg
id           └──┘        └──┘      └─┘                   └────────────┘ └┘
src           └──┘          └──┘      └─┘                          └────────────┘
typ          └──┘        └──┘      └─┘                   └────────────┘ └┘
doc           └──┘          └──┘
312    ... = ((@prod.swap α α) <$> (𝓤 α)).lift (λs:set (α×α), g {y | (x, y) ∈ s}) : by rw [←uniformity_eq_symm]
id              └───────┘    └─┘     └──┘      └─┘                           └────────────────┘
src             └───────┘      └─┘      └──┘      └─┘                             └───┘└────────────────┘└─
typ             └───────┘    └─┘     └──┘      └─┘                      └───┘└────────────────┘└─
doc             └───────┘               └──┘                                          └───┘                  └─
txt                                                                                    └───┘                  └─
par                                                                                    └───┘                  └─
pid                                                                                      └─┘                  
st                                                                                    └──────────────────────┘
313    ... = (𝓤 α).lift (λs:set (α×α), g {y | (x, y) ∈ image prod.swap s}) :
id              └──┘      └─┘              └───┘ └───────┘ 
src  ─┘          └──┘      └─┘                    └───┘ └───────┘
typ  ─┘         └──┘      └─┘              └───┘ └───────┘ 
doc  ─┘          └──┘                                       └───────┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
314      map_lift_eq2 $ hg.comp monotone_preimage
id       └──────────┘   └┘└───┘ └───────────────┘
src      └──────────┘     └───┘ └───────────────┘
typ      └──────────┘   └┘└───┘ └───────────────┘
315    ... = _ : by simp [image_swap_eq_preimage_swap]
id                        └─────────────────────────┘
src                 └────┘└─────────────────────────┘└─
typ                 └────┘└─────────────────────────┘└─
doc                 └────┘                           └─
txt                 └────┘                           └─
par                 └────┘                           └─
pid                                                
st                 └───────────────────────────────────
316  
src  
typ  
doc  
txt  
par  
pid  
st   
317  lemma nhds_nhds_eq_uniformity_uniformity_prod {a b : α} :
id                                                        
typ                                                       
318    filter.prod (𝓝 a) (𝓝 b) =
id     └─────────┘         
src    └─────────┘           
typ    └─────────┘         
doc    └─────────┘       
319    (𝓤 α).lift (λs:set (α×α), (𝓤 α).lift' (λt:set (α×α),
id        └──┘      └─┘        └───┘      └─┘  
src        └──┘      └─┘           └───┘      └─┘   
typ       └──┘      └─┘        └───┘      └─┘  
doc        └──┘                     └───┘
320      set.prod {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ t})) :=
id       └──────┘                           
src      └──────┘                                 
typ      └──────┘                           
doc      └──────┘
321  begin
st   └─────
322    rw [prod_def],
id         └──────┘
src    └──┘└──────┘
typ    └──┘└──────┘
doc    └──┘        
txt    └──┘        
par    └──┘        
pid      └┘        
st   ─────────────┘└──
323    show (𝓝 a).lift (λs:set α, (𝓝 b).lift (λt:set α, principal (set.prod s t))) = _,
id                       └─┘                  └─┘   └───────┘  └──────┘        
src    └───┘  └─────┘  └┘    └┘   └─────┘  └┘└─┘ └┘└───────┘ └──────┘  └──┘└┘
typ    └───┘ └─────┘  └┘└─┘ └┘  └─────┘  └┘└─┘└┘└───────┘ └──────┘  └──┘└┘
doc    └───┘  └─────┘  └┘    └┘   └─────┘  └┘    └┘└───────┘ └──────┘  └──┘ └┘
txt    └───┘   └─────┘  └┘    └┘   └─────┘  └┘    └┘                    └──┘ └┘
par    └───┘   └─────┘  └┘    └┘   └─────┘  └┘    └┘                    └──┘ └┘
pid    └───┘   └─────┘  └┘    └┘   └─────┘  └┘    └┘                    └──┘ └┘
st   ────────────────────────────────────────────────────────────────────────────────┘└─
324    rw [lift_nhds_right],
id         └─────────────┘
src    └──┘└─────────────┘
typ    └──┘└─────────────┘
doc    └──┘               
txt    └──┘               
par    └──┘               
pid      └┘               
st   ────────────────────┘└──
325    apply congr_arg, funext s,
id           └───────┘
src    └────┘└───────┘  └──────┘
typ    └────┘└───────┘  └──────┘
doc    └────┘           └──────┘
txt    └────┘           └──────┘
par    └────┘           └──────┘
pid                          └┘
st   ────────────────┘└────────┘└─
326    rw [lift_nhds_left],
id         └────────────┘
src    └──┘└────────────┘
typ    └──┘└────────────┘
doc    └──┘              
txt    └──┘              
par    └──┘              
pid      └┘              
st   ───────────────────┘└──
327    refl,
src    └──┘
typ    └──┘
doc    └──┘
txt    └──┘
par    └──┘
st   ─────┘└─
328    exact monotone_principal.comp (monotone_prod monotone_const monotone_id),
id           └─────────────────────┘  └───────────┘ └────────────┘ └─────────┘
src    └────┘└─────────────────────┘ └───────────┘└────────────┘└─────────┘
typ    └────┘└─────────────────────┘ └───────────┘└────────────┘└─────────┘
doc    └────┘                                                              
txt    └────┘                                                              
par    └────┘                                                              
pid                                                                       
st   ─────────────────────────────────────────────────────────────────────────┘└─
329    exact (monotone_lift' monotone_const $ monotone_lam $
id            └────────────┘                  └──────────┘
src    └────┘ └────────────┘               └──────────┘ 
typ    └────┘ └────────────┘               └──────────┘ 
doc    └────┘                                           
txt    └────┘                                           
par    └────┘                                           
pid                                                    
st   ────────────────────────────────────────────────────────
330      assume x, monotone_prod monotone_id monotone_const)
id                 └───────────┘ └─────────┘ └────────────┘
src  ───┘      └──┘└───────────┘└─────────┘└────────────┘└┘
typ  ───┘      └──┘└───────────┘└─────────┘└────────────┘└┘
doc  ───┘      └──┘                                      └┘
txt  ───┘      └──┘                                      └┘
par  ───┘      └──┘                                      └┘
pid  ───┘      └──┘                                      
st   ───────────────────────────────────────────────────────┘
331  end
st   └─┘
332  
333  lemma nhds_eq_uniformity_prod {a b : α} :
id                                        
typ                                       
334    𝓝 (a, b) =
id          
src           
typ         
doc    
335    (𝓤 α).lift' (λs:set (α×α), set.prod {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ s}) :=
id        └───┘      └─┘     └──────┘                           
src        └───┘      └─┘       └──────┘                                 
typ       └───┘      └─┘     └──────┘                           
doc        └───┘                 └──────┘
336  begin
st   └─────
337    rw [nhds_prod_eq, nhds_nhds_eq_uniformity_uniformity_prod, lift_lift'_same_eq_lift'],
id         └──────────┘  └─────────────────────────────────────┘  └──────────────────────┘
src    └──┘└──────────┘└┘└─────────────────────────────────────┘└┘└──────────────────────┘
typ    └──┘└──────────┘└┘└─────────────────────────────────────┘└┘└──────────────────────┘
doc    └──┘            └┘                                       └┘                        
txt    └──┘            └┘                                       └┘                        
par    └──┘            └┘                                       └┘                        
pid      └┘            └┘                                       └┘                        
st   ─────────────────┘└───────────────────────────────────────┘└────────────────────────┘└──
338    { intro s, exact monotone_prod monotone_const monotone_preimage },
id                      └───────────┘ └────────────┘ └───────────────┘
src      └─────┘  └────┘└───────────┘└────────────┘└───────────────┘
typ      └─────┘  └────┘└───────────┘└────────────┘└───────────────┘
doc      └─────┘  └────┘                                            
txt      └─────┘  └────┘                                            
par      └─────┘  └────┘                                            
pid           └┘                                                   
st   ───┘└─────┘└─────────────────────────────────────────────────────┘└┘
339    { intro t, exact monotone_prod monotone_preimage monotone_const }
id                      └───────────┘ └───────────────┘ └────────────┘
src      └─────┘  └────┘└───────────┘└───────────────┘└────────────┘
typ      └─────┘  └────┘└───────────┘└───────────────┘└────────────┘
doc      └─────┘  └────┘                                            
txt      └─────┘  └────┘                                            
par      └─────┘  └────┘                                            
pid           └┘                                                   
st   ──────────┘└─────────────────────────────────────────────────────┘└─
340  end
st   ──┘
341  
342  lemma nhdset_of_mem_uniformity {d : set (α×α)} (s : set (α×α)) (hd : d ∈ 𝓤 α) :
id                                       └─┘          └─┘              
src                                      └─┘            └─┘                
typ                                      └─┘          └─┘              
doc                                                                           
343    ∃(t : set (α×α)), is_open t ∧ s ⊆ t ∧ t ⊆ {p | ∃x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d} :=
id          └─┘     └─────┘                                   
src         └─┘       └─────┘                                                 
typ         └─┘     └─────┘                                   
doc                      └─────┘
344  let cl_d := {p:α×α | ∃x y, (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d} in
id       └──┘                                
src                                                     
typ      └──┘                                
345  have ∀p ∈ s, ∃t ⊆ cl_d, is_open t ∧ p ∈ t, from
id                 └──┘ └─────┘     
src                        └─────┘      
typ                └──┘ └─────┘     
doc                          └─────┘
346    assume ⟨x, y⟩ hp, mem_nhds_sets_iff.mp $
id                └┘  └───────────────┘└─┘
src                      └───────────────┘└─┘
typ               └┘  └───────────────┘└─┘
347    show cl_d ∈ 𝓝 (x, y),
id          └──┘   
src                
typ         └──┘   
doc                
348    begin
st     └─────
349      rw [nhds_eq_uniformity_prod, mem_lift'_sets],
id           └─────────────────────┘  └────────────┘
src      └──┘└─────────────────────┘└┘└────────────┘
typ      └──┘└─────────────────────┘└┘└────────────┘
doc      └──┘                       └┘              
txt      └──┘                       └┘              
par      └──┘                       └┘              
pid        └┘                       └┘              
st   ──────────────────────────────┘└──────────────┘└──
350      exact ⟨d, hd, assume ⟨a, b⟩ ⟨ha, hb⟩, ⟨x, y, ha, hp, hb⟩⟩,
id                └┘                 └┘  └┘            └┘
src      └────┘  └┘  └┘      └┘ └┘ └─┘  └┘  └─┘  └┘ └┘  └┘  └┘  └┘
typ      └────┘ └┘└┘└┘      └┘ └┘ └─┘└┘└┘└┘└─┘ └┘└┘  └┘└┘└┘  └┘
doc      └────┘  └┘  └┘      └┘ └┘ └─┘  └┘  └─┘  └┘ └┘  └┘  └┘  └┘
txt      └────┘  └┘  └┘      └┘ └┘ └─┘  └┘  └─┘  └┘ └┘  └┘  └┘  └┘
par      └────┘  └┘  └┘      └┘ └┘ └─┘  └┘  └─┘  └┘ └┘  └┘  └┘  └┘
pid             └┘  └┘      └┘ └┘ └─┘  └┘  └─┘  └┘ └┘  └┘  └┘  └┘
st   ────────────────────────────────────────────────────────────┘└─
351      exact monotone_prod monotone_preimage monotone_preimage
id             └───────────┘                   └───────────────┘
src      └────┘└───────────┘                 └───────────────┘
typ      └────┘└───────────┘                 └───────────────┘
doc      └────┘                                               
txt      └────┘                                               
par      └────┘                                               
pid                                                          
st   ────────────────────────────────────────────────────────────
352    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
353  have ∃t:(Π(p:α×α) (h:p ∈ s), set (α×α)),
id                        └─┘    
src                            └─┘      
typ                       └─┘    
354      ∀p, ∀h:p ∈ s, t p h ⊆ cl_d ∧ is_open (t p h) ∧ p ∈ t p h,
id                     └──┘  └─────┘           
src                                └─────┘            
typ                    └──┘  └─────┘           
doc                                   └─────┘
355    by simp [classical.skolem] at this; simp; assumption,
id              └──────────────┘
src       └────┘└──────────────┘└───────┘  └──┘  └────────┘
typ       └────┘└──────────────┘└───────┘  └──┘  └────────┘
doc       └────┘                └───────┘  └──┘  └────────┘
txt       └────┘                └───────┘  └──┘  └────────┘
par       └────┘                └───────┘  └──┘  └────────┘
pid                           └─────┘
st       └────────────────────────────────────────────────┘
356  match this with
id         └──┘
typ        └──┘
357  | ⟨t, ht⟩ :=
id        └┘
typ       └┘
358    ⟨(⋃ p:α×α, ⋃ h : p ∈ s, t p h : set (α×α)),
id                         └─┘  
src                              └─┘   
typ                        └─┘  
doc                       
359      is_open_Union $ assume (p:α×α), is_open_Union $ assume hp, (ht p hp).right.left,
id       └───────────┘                └───────────┘          └┘       └┘ └───┘ └──┘
src      └───────────┘                  └───────────┘                       └───┘ └──┘
typ      └───────────┘                └───────────┘          └┘       └┘ └───┘ └──┘
360      assume ⟨a, b⟩ hp, begin simp; exact ⟨a, b, hp, (ht (a,b) hp).right.right⟩ end,
id                    └┘                                └┘    └┘
src                              └──┘  └────┘  └┘ └┘  └┘     └┘  └─────────────┘
typ                   └┘        └──┘  └────┘  └┘ └┘  └┘ └┘└┘└┘└─────────────┘
doc                              └──┘  └────┘  └┘ └┘  └┘      └┘  └─────────────┘
txt                              └──┘  └────┘  └┘ └┘  └┘      └┘  └─────────────┘
par                              └──┘  └────┘  └┘ └┘  └┘      └┘  └─────────────┘
pid                                           └┘ └┘  └┘      └┘  └────────────┘
st                         └──────────────────────────────────────────────────────┘└─┘
361      Union_subset $ assume p, Union_subset $ assume hp, (ht p hp).left⟩
id       └──────────┘            └──────────┘          └┘       └┘ └──┘
src      └──────────┘             └──────────┘                       └──┘
typ      └──────────┘            └──────────┘          └┘       └┘ └──┘
362  end
363  
364  lemma closure_eq_inter_uniformity {t : set (α×α)} :
id                                          └─┘  
src                                         └─┘   
typ                                         └─┘  
365    closure t = (⋂ d ∈ 𝓤 α, comp_rel d (comp_rel t d)) :=
id     └─────┘          └──────┘   └──────┘  
src    └─────┘             └──────┘    └──────┘
typ    └─────┘          └──────┘   └──────┘  
doc    └─────┘              └──────┘    └──────┘
366  set.ext $ assume ⟨a, b⟩,
id   └─────┘            
src  └─────┘
typ  └─────┘            
367  calc (a, b) ∈ closure t ↔ (𝓝 (a, b) ⊓ principal t ≠ ⊥) : by simp [closure_eq_nhds]
id               └─────┘             └───────┘                └─────────────┘
src              └─────┘              └───────┘           └────┘└─────────────┘└─
typ              └─────┘             └───────┘          └────┘└─────────────┘└─
doc                └─────┘                └───────┘             └────┘               └─
txt                                                              └────┘               └─
par                                                              └────┘               └─
pid                                                                                 
st                                                              └───────────────────────
368    ... ↔ (((@prod.swap α α) <$> 𝓤 α).lift'
id               └───────┘    └─┘   └───┘
src  ─┘          └───────┘      └─┘    └───┘
typ  ─┘          └───────┘    └─┘   └───┘
doc  ─┘          └───────┘             └───┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
369        (λ (s : set (α × α)), set.prod {x : α | (x, a) ∈ s} {y : α | (b, y) ∈ s}) ⊓ principal t ≠ ⊥) :
id                 └─┘        └──────┘                                 └───────┘   
src                └─┘          └──────┘                                       └───────┘    
typ                └─┘        └──────┘                                 └───────┘   
doc                              └──────┘                                              └───────┘
370      by rw [←uniformity_eq_symm, nhds_eq_uniformity_prod]
id               └────────────────┘  └─────────────────────┘
src         └───┘└────────────────┘└┘└─────────────────────┘└─
typ         └───┘└────────────────┘└┘└─────────────────────┘└─
doc         └───┘                  └┘                       └─
txt         └───┘                  └┘                       └─
par         └───┘                  └┘                       └─
pid           └─┘                  └┘                       
st         └──────────────────────┘└───────────────────────┘
371    ... ↔ ((map (@prod.swap α α) (𝓤 α)).lift'
id             └─┘   └───────┘        └───┘
src  ─┘        └─┘   └───────┘           └───┘
typ  ─┘        └─┘   └───────┘        └───┘
doc  ─┘        └─┘   └───────┘           └───┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
372        (λ (s : set (α × α)), set.prod {x : α | (x, a) ∈ s} {y : α | (b, y) ∈ s}) ⊓ principal t ≠ ⊥) :
id                 └─┘        └──────┘                                 └───────┘   
src                └─┘          └──────┘                                       └───────┘    
typ                └─┘        └──────┘                                 └───────┘   
doc                              └──────┘                                              └───────┘
373      by refl
src         └────
typ         └────
doc         └────
txt         └────
par         └────
pid             
st         └─────
374    ... ↔ ((𝓤 α).lift'
id               └───┘
src  ─┘           └───┘
typ  ─┘          └───┘
doc  ─┘           └───┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
375        (λ (s : set (α × α)), set.prod {y : α | (a, y) ∈ s} {x : α | (x, b) ∈ s}) ⊓ principal t ≠ ⊥) :
id                 └─┘        └──────┘                                 └───────┘   
src                └─┘          └──────┘                                       └───────┘    
typ                └─┘        └──────┘                                 └───────┘   
doc                              └──────┘                                              └───────┘
376    begin
st     └─────
377      rw [map_lift'_eq2],
id           └───────────┘
src      └──┘└───────────┘
typ      └──┘└───────────┘
doc      └──┘             
txt      └──┘             
par      └──┘             
pid        └┘             
st   ────────────────────┘└──
378      simp [image_swap_eq_preimage_swap, function.comp],
id             └─────────────────────────┘  └───────────┘
src      └────┘└─────────────────────────┘└┘└───────────┘
typ      └────┘└─────────────────────────┘└┘└───────────┘
doc      └────┘                           └┘             
txt      └────┘                           └┘             
par      └────┘                           └┘             
pid                                     └┘             
st   ────────────────────────────────────────────────────┘└─
379      exact monotone_prod monotone_preimage monotone_preimage
id             └───────────┘                   └───────────────┘
src      └────┘└───────────┘                 └───────────────┘
typ      └────┘└───────────┘                 └───────────────┘
doc      └────┘                                               
txt      └────┘                                               
par      └────┘                                               
pid                                                          
st   ────────────────────────────────────────────────────────────
380    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
381    ... ↔ (∀s ∈ 𝓤 α, (set.prod {y : α | (a, y) ∈ s} {x : α | (x, b) ∈ s} ∩ t).nonempty) :
id                    └──────┘                                 └──────┘
src                     └──────┘                                        └──────┘
typ                   └──────┘                                 └──────┘
doc                     └──────┘                                               └──────┘
382    begin
st     └─────
383      rw [lift'_inf_principal_eq, lift'_ne_bot_iff],
id           └────────────────────┘  └──────────────┘
src      └──┘└────────────────────┘└┘└──────────────┘
typ      └──┘└────────────────────┘└┘└──────────────┘
doc      └──┘                      └┘                
txt      └──┘                      └┘                
par      └──┘                      └┘                
pid        └┘                      └┘                
st   ─────────────────────────────┘└────────────────┘└──
384      exact monotone_inter (monotone_prod monotone_preimage monotone_preimage) monotone_const
id             └────────────┘  └───────────┘                   └───────────────┘  └────────────┘
src      └────┘└────────────┘ └───────────┘                 └───────────────┘└┘└────────────┘
typ      └────┘└────────────┘ └───────────┘                 └───────────────┘└┘└────────────┘
doc      └────┘                                                              └┘              
txt      └────┘                                                              └┘              
par      └────┘                                                              └┘              
pid                                                                         └┘              
st   ────────────────────────────────────────────────────────────────────────────────────────────
385    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
386    ... ↔ (∀ s ∈ 𝓤 α, (a, b) ∈ comp_rel s (comp_rel t s)) :
id                           └──────┘   └──────┘  
src                            └──────┘    └──────┘
typ                          └──────┘   └──────┘  
doc                              └──────┘    └──────┘
387      forall_congr $ assume s, forall_congr $ assume hs,
id       └──────────┘            └──────────┘          └┘
src      └──────────┘             └──────────┘
typ      └──────────┘            └──────────┘          └┘
388      ⟨assume ⟨⟨x, y⟩, ⟨⟨hx, hy⟩, hxyt⟩⟩, ⟨x, hx, y, hxyt, hy⟩,
id                       └┘  └┘   └──┘
typ                      └┘  └┘   └──┘
389        assume ⟨x, hx, y, hxyt, hy⟩, ⟨⟨x, y⟩, ⟨⟨hx, hy⟩, hxyt⟩⟩⟩
id                  └┘    └──┘  └┘
typ                 └┘    └──┘  └┘
390    ... ↔ _ : by simp
src                 └────
typ                 └────
doc                 └────
txt                 └────
par                 └────
pid                     
st                 └─────
391  
src  
typ  
doc  
txt  
par  
pid  
st   
392  lemma uniformity_eq_uniformity_closure : 𝓤 α = (𝓤 α).lift' closure :=
id                                                  └───┘  └─────┘
src                                                   └───┘  └─────┘
typ                                                 └───┘  └─────┘
doc                                                    └───┘  └─────┘
393  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
394    (le_infi $ assume s, le_infi $ assume hs, by simp; filter_upwards [hs] subset_closure)
id      └─────┘            └─────┘          └┘                               └────────────┘
src     └─────┘             └─────┘                 └──┘  └──────────────┘  └┘└────────────┘
typ     └─────┘            └─────┘          └┘     └──┘  └──────────────┘  └┘└────────────┘
doc                                                 └──┘  └──────────────┘  └┘
txt                                                 └──┘  └──────────────┘  └┘
par                                                 └──┘  └──────────────┘  └┘
pid                                                                     └┘  
st                                                 └───────────────────────────────────────┘
395    (calc (𝓤 α).lift' closure ≤ (𝓤 α).lift' (λd, comp_rel d (comp_rel d d)) :
id              └───┘  └─────┘      └───┘      └──────┘   └──────┘  
src              └───┘  └─────┘       └───┘       └──────┘    └──────┘
typ             └───┘  └─────┘      └───┘      └──────┘   └──────┘  
doc              └───┘  └─────┘       └───┘       └──────┘    └──────┘
396        lift'_mono' (by intros s hs; rw [closure_eq_inter_uniformity]; exact bInter_subset_of_mem hs)
id         └─────────┘                      └─────────────────────────┘         └──────────────────┘ └┘
src        └─────────┘     └─────────┘  └──┘└─────────────────────────┘  └────┘└──────────────────┘
typ        └─────────┘     └─────────┘  └──┘└─────────────────────────┘  └────┘└──────────────────┘└┘
doc                        └─────────┘  └──┘                             └────┘                    
txt                        └─────────┘  └──┘                             └────┘                    
par                        └─────────┘  └──┘                             └────┘                    
pid                              └───┘    └┘                                                      
st                        └────────────────┘└─────────────────────────┘└─────────────────────────────┘
397      ... ≤ (𝓤 α) : comp_le_uniformity3)
id                   └─────────────────┘
src                   └─────────────────┘
typ                  └─────────────────┘
doc             
398  
399  lemma uniformity_eq_uniformity_interior : 𝓤 α = (𝓤 α).lift' interior :=
id                                                   └───┘  └──────┘
src                                                    └───┘  └──────┘
typ                                                  └───┘  └──────┘
doc                                                     └───┘  └──────┘
400  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
401    (le_infi $ assume d, le_infi $ assume hd,
id      └─────┘            └─────┘          └┘
src     └─────┘             └─────┘
typ     └─────┘            └─────┘          └┘
402      let ⟨s, hs, hs_comp⟩ := (mem_lift'_sets $
id       └─┘    └┘  └─────┘      └────────────┘
src                               └────────────┘
typ      └─┘    └┘  └─────┘      └────────────┘
403        monotone_comp_rel monotone_id $ monotone_comp_rel monotone_id monotone_id).mp (comp_le_uniformity3 hd) in
id         └───────────────┘ └─────────┘   └───────────────┘ └─────────┘ └─────────┘ └┘   └─────────────────┘ └┘
src        └───────────────┘ └─────────┘   └───────────────┘ └─────────┘ └─────────┘ └┘   └─────────────────┘
typ        └───────────────┘ └─────────┘   └───────────────┘ └─────────┘ └─────────┘ └┘   └─────────────────┘ └┘
404      let ⟨t, ht, hst, ht_comp⟩ := nhdset_of_mem_uniformity s hs in
id       └─┘    └┘  └─┘  └─────┘     └──────────────────────┘
src                                   └──────────────────────┘
typ      └─┘    └┘  └─┘  └─────┘     └──────────────────────┘
405      have s ⊆ interior d, from
id               └──────┘ 
src              └──────┘
typ              └──────┘ 
doc               └──────┘
406        calc s ⊆ t : hst
407         ... ⊆ interior d : (subset_interior_iff_subset_of_open ht).mpr $
id                └──────┘     └────────────────────────────────┘    └─┘
src               └──────┘      └────────────────────────────────┘    └─┘
typ               └──────┘     └────────────────────────────────┘    └─┘
doc               └──────┘
408          assume x, assume : x ∈ t, let ⟨x, y, h₁, h₂, h₃⟩ := ht_comp this in hs_comp ⟨x, h₁, y, h₂, h₃⟩,
id                                  └─┘      └┘  └┘  └┘             └──┘
src                               
typ                                 └─┘      └┘  └┘  └┘             └──┘
409      have interior d ∈ 𝓤 α, by filter_upwards [hs] this,
id            └──────┘                             └──┘
src           └──────┘           └──────────────┘  └┘
typ           └──────┘         └──────────────┘  └┘└──┘
doc           └──────┘            └──────────────┘  └┘
txt                                └──────────────┘  └┘
par                                └──────────────┘  └┘
pid                                              └┘  
st                                └───────────────────────┘
410      by simp [this])
id                └──┘
src         └────┘    
typ         └────┘└──┘
doc         └────┘    
txt         └────┘    
par         └────┘    
pid                 
st         └──────────┘
411    (assume s hs, ((𝓤 α).lift' interior).sets_of_superset (mem_lift' hs) interior_subset)
id              └┘      └───┘  └──────┘ └──────────────┘   └───────┘ └┘  └─────────────┘
src                       └───┘  └──────┘ └──────────────┘   └───────┘     └─────────────┘
typ             └┘      └───┘  └──────┘ └──────────────┘   └───────┘ └┘  └─────────────┘
doc                       └───┘  └──────┘
412  
413  lemma interior_mem_uniformity {s : set (α × α)} (hs : s ∈ 𝓤 α) :
id                                      └─┘                
src                                     └─┘                  
typ                                     └─┘                
doc                                                            
414    interior s ∈ 𝓤 α :=
id     └──────┘    
src    └──────┘    
typ    └──────┘    
doc    └──────┘     
415  by rw [uniformity_eq_uniformity_interior]; exact mem_lift' hs
id          └───────────────────────────────┘         └───────┘ └┘
src     └──┘└───────────────────────────────┘  └────┘└───────┘  
typ     └──┘└───────────────────────────────┘  └────┘└───────┘└┘
doc     └──┘                                   └────┘           
txt     └──┘                                   └────┘           
par     └──┘                                   └────┘           
pid       └┘                                                   
st     └────────────────────────────────────┘└────────────────────
416  
src  
typ  
doc  
txt  
par  
pid  
st   
417  lemma mem_uniformity_is_closed {s : set (α×α)} (h : s ∈ 𝓤 α) :
id                                       └─┘             
src                                      └─┘               
typ                                      └─┘             
doc                                                          
418    ∃t ∈ 𝓤 α, is_closed t ∧ t ⊆ s :=
id          └───────┘     
src           └───────┘      
typ         └───────┘     
doc             └───────┘
419  have s ∈ (𝓤 α).lift' closure, by rwa [uniformity_eq_uniformity_closure] at h,
id             └───┘  └─────┘          └──────────────────────────────┘
src              └───┘  └─────┘     └───┘└──────────────────────────────┘└────┘
typ            └───┘  └─────┘     └───┘└──────────────────────────────┘└────┘
doc               └───┘  └─────┘     └───┘                                └────┘
txt                                   └───┘                                └────┘
par                                   └───┘                                └────┘
pid                                      └┘                                └───┘
st                                   └────────────────────────────────────┘└───┘
420  have ∃ t ∈ 𝓤 α, closure t ⊆ s,
id              └─────┘   
src               └─────┘   
typ             └─────┘   
doc                 └─────┘
421    by rwa [mem_lift'_sets] at this; apply closure_mono,
id             └────────────┘                 └──────────┘
src       └───┘└────────────┘└───────┘  └────┘└──────────┘
typ       └───┘└────────────┘└───────┘  └────┘└──────────┘
doc       └───┘              └───────┘  └────┘
txt       └───┘              └───────┘  └────┘
par       └───┘              └───────┘  └────┘
pid          └┘              └──────┘       
st       └──────────────────┘└──────────────────────────┘
422  let ⟨t, ht, hst⟩ := this in
id   └─┘    └┘  └─┘     └──┘
typ  └─┘    └┘  └─┘     └──┘
423  ⟨closure t, (𝓤 α).sets_of_superset ht subset_closure, is_closed_closure, hst⟩
id    └─────┘       └──────────────┘     └────────────┘  └───────────────┘
src   └─────┘        └──────────────┘     └────────────┘  └───────────────┘
typ   └─────┘       └──────────────┘     └────────────┘  └───────────────┘
doc   └─────┘     
424  
425  /- uniform continuity -/
426  
427  def uniform_continuous [uniform_space β] (f : α → β) :=
id                           └───────────┘           
src                          └───────────┘
typ                          └───────────┘           
doc                          └───────────┘
428  tendsto (λx:α×α, (f x.1, f x.2)) (𝓤 α) (𝓤 β)
id   └─────┘                      
src  └─────┘                            
typ  └─────┘                      
doc  └─────┘                                
429  
430  theorem uniform_continuous_def [uniform_space β] {f : α → β} :
id                                   └───────────┘           
src                                  └───────────┘
typ                                  └───────────┘           
doc                                  └───────────┘
431    uniform_continuous f ↔ ∀ r ∈ 𝓤 β,
id     └────────────────┘         
src    └────────────────┘          
typ    └────────────────┘         
doc                                 
432      {x : α × α | (f x.1, f x.2) ∈ r} ∈ 𝓤 α :=
id                             
src                                  
typ                            
doc                                         
433  iff.rfl
id   └─────┘
src  └─────┘
typ  └─────┘
434  
435  lemma uniform_continuous_of_const [uniform_space β] {c : α → β} (h : ∀a b, c a = c b) :
id                                      └───────────┘                          
src                                     └───────────┘                               
typ                                     └───────────┘                          
doc                                     └───────────┘
436    uniform_continuous c :=
id     └────────────────┘ 
src    └────────────────┘
typ    └────────────────┘ 
437  have (λ (x : α × α), (c (x.fst), c (x.snd))) ⁻¹' id_rel = univ, from
id                       └──┘     └──┘    └─┘ └────┘  └──┘
src                          └──┘       └──┘    └─┘ └────┘  └──┘
typ                      └──┘     └──┘    └─┘ └────┘  └──┘
doc                                               └─┘ └────┘
438    eq_univ_iff_forall.2 $ assume ⟨a, b⟩, h a b,
id     └────────────────┘                
src    └────────────────┘
typ    └────────────────┘                
439  le_trans (map_le_iff_le_comap.2 $ by simp [comap_principal, this, univ_mem_sets]) refl_le_uniformity
id   └──────┘  └─────────────────┘             └─────────────┘  └──┘  └───────────┘   └────────────────┘
src  └──────┘  └─────────────────┘       └────┘└─────────────┘└┘    └┘└───────────┘  └────────────────┘
typ  └──────┘  └─────────────────┘       └────┘└─────────────┘└┘└──┘└┘└───────────┘  └────────────────┘
doc                                       └────┘               └┘    └┘             
txt                                       └────┘               └┘    └┘             
par                                       └────┘               └┘    └┘             
pid                                                          └┘    └┘             
st                                       └──────────────────────────────────────────┘
440  
441  lemma uniform_continuous_id : uniform_continuous (@id α) :=
id                                 └────────────────┘   └┘ 
src                                └────────────────┘   └┘
typ                                └────────────────┘   └┘ 
442  by simp [uniform_continuous]; exact tendsto_id
id            └────────────────┘         └────────┘
src     └────┘└────────────────┘  └────┘└────────┘
typ     └────┘└────────────────┘  └────┘└────────┘
doc     └────┘                    └────┘          
txt     └────┘                    └────┘          
par     └────┘                    └────┘          
pid                                            
st     └────────────────────────────────────────────
443  
src  
typ  
doc  
txt  
par  
pid  
st   
444  lemma uniform_continuous_const [uniform_space β] {b : β} : uniform_continuous (λa:α, b) :=
id                                   └───────────┘            └────────────────┘       
src                                  └───────────┘              └────────────────┘
typ                                  └───────────┘            └────────────────┘       
doc                                  └───────────┘
445  @tendsto_const_uniformity _ _ _ b (𝓤 α)
id    └──────────────────────┘          
src   └──────────────────────┘          
typ   └──────────────────────┘          
doc                                     
446  
447  lemma uniform_continuous.comp [uniform_space β] [uniform_space γ] {g : β → γ} {f : α → β}
id                                  └───────────┘    └───────────┘                     
src                                 └───────────┘     └───────────┘
typ                                 └───────────┘    └───────────┘                     
doc                                 └───────────┘     └───────────┘
448    (hg : uniform_continuous g) (hf : uniform_continuous f) : uniform_continuous (g ∘ f) :=
id           └────────────────┘         └────────────────┘     └────────────────┘    
src          └────────────────┘          └────────────────┘      └────────────────┘    
typ          └────────────────┘         └────────────────┘     └────────────────┘    
449  hg.comp hf
id   └┘└───┘ └┘
src    └───┘
typ  └┘└───┘ └┘
450  end uniform_space
451  end
452  
453  open_locale uniformity
454  
455  section constructions
456  variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} {ι : Sort*}
457  
458  instance : partial_order (uniform_space α) :=
id              └───────────┘  └───────────┘ 
src             └───────────┘  └───────────┘
typ             └───────────┘  └───────────┘ 
doc                            └───────────┘
459  { le          := λt s, t.uniformity ≤ s.uniformity,
id                       └─────────┘  └─────────┘
src                         └─────────┘   └─────────┘
typ                      └─────────┘  └─────────┘
460    le_antisymm := assume t s h₁ h₂, uniform_space_eq $ le_antisymm h₁ h₂,
id                             └┘ └┘  └──────────────┘   └─────────┘ └┘ └┘
src                                     └──────────────┘   └─────────┘
typ                            └┘ └┘  └──────────────┘   └─────────┘ └┘ └┘
461    le_refl     := assume t, le_refl _,
id                             └─────┘
src                             └─────┘
typ                            └─────┘
462    le_trans    := assume a b c h₁ h₂, le_trans h₁ h₂ }
id                              └┘ └┘  └──────┘ └┘ └┘
src                                       └──────┘
typ                             └┘ └┘  └──────┘ └┘ └┘
463  
464  instance : has_Inf (uniform_space α) :=
id              └─────┘  └───────────┘ 
src             └─────┘  └───────────┘
typ             └─────┘  └───────────┘ 
doc             └─────┘  └───────────┘
465  ⟨assume s, uniform_space.of_core {
id             └───────────────────┘
src             └───────────────────┘
typ            └───────────────────┘
466    uniformity := (⨅u∈s, @uniformity α u),
id                       └────────┘  
src                        └────────┘
typ                      └────────┘  
doc                        └────────┘
467    refl       := le_infi $ assume u, le_infi $ assume hu, u.refl,
id                   └─────┘            └─────┘          └┘  └───┘
src                  └─────┘             └─────┘               └───┘
typ                  └─────┘            └─────┘          └┘  └───┘
468    symm       := le_infi $ assume u, le_infi $ assume hu,
id                   └─────┘            └─────┘          └┘
src                  └─────┘             └─────┘
typ                  └─────┘            └─────┘          └┘
469      le_trans (map_mono $ infi_le_of_le _ $ infi_le _ hu) u.symm,
id       └──────┘  └──────┘   └───────────┘     └─────┘   └┘  └───┘
src      └──────┘  └──────┘   └───────────┘     └─────┘        └───┘
typ      └──────┘  └──────┘   └───────────┘     └─────┘   └┘  └───┘
470    comp       := le_infi $ assume u, le_infi $ assume hu,
id                   └─────┘            └─────┘          └┘
src                  └─────┘             └─────┘
typ                  └─────┘            └─────┘          └┘
471      le_trans (lift'_mono (infi_le_of_le _ $ infi_le _ hu) $ le_refl _) u.comp }⟩
id       └──────┘  └────────┘  └───────────┘     └─────┘   └┘    └─────┘    └───┘
src      └──────┘  └────────┘  └───────────┘     └─────┘         └─────┘     └───┘
typ      └──────┘  └────────┘  └───────────┘     └─────┘   └┘    └─────┘    └───┘
472  
473  private lemma Inf_le {tt : set (uniform_space α)} {t : uniform_space α} (h : t ∈ tt) :
id                              └─┘  └───────────┘         └───────────┘          └┘
src                             └─┘  └───────────┘          └───────────┘           
typ                             └─┘  └───────────┘         └───────────┘          └┘
doc                                  └───────────┘          └───────────┘
474    Inf tt ≤ t :=
id     └─┘ └┘  
src    └─┘    
typ    └─┘ └┘  
doc    └─┘
475  show (⨅u∈tt, @uniformity α u) ≤ t.uniformity,
id          └┘  └────────┘     └─────────┘
src              └────────┘        └─────────┘
typ         └┘  └────────┘     └─────────┘
doc              └────────┘
476    from infi_le_of_le t $ infi_le _ h
id          └───────────┘    └─────┘   
src         └───────────┘     └─────┘
typ         └───────────┘    └─────┘   
477  
478  private lemma le_Inf {tt : set (uniform_space α)} {t : uniform_space α} (h : ∀t'∈tt, t ≤ t') :
id                              └─┘  └───────────┘         └───────────┘         └┘ └┘    └┘
src                             └─┘  └───────────┘          └───────────┘                   
typ                             └─┘  └───────────┘         └───────────┘         └┘ └┘    └┘
doc                                  └───────────┘          └───────────┘
479    t ≤ Inf tt :=
id       └─┘ └┘
src       └─┘
typ      └─┘ └┘
doc        └─┘
480  show t.uniformity ≤ (⨅u∈tt, @uniformity α u),
id        └─────────┘    └┘  └────────┘  
src        └─────────┘         └────────┘
typ       └─────────┘    └┘  └────────┘  
doc                             └────────┘
481    from le_infi $ assume t', le_infi $ assume ht', h t' ht'
id          └─────┘          └┘  └─────┘          └─┘   └┘ └─┘
src         └─────┘              └─────┘
typ         └─────┘          └┘  └─────┘          └─┘   └┘ └─┘
482  
483  instance : has_top (uniform_space α) :=
id              └─────┘  └───────────┘ 
src             └─────┘  └───────────┘
typ             └─────┘  └───────────┘ 
doc             └─────┘  └───────────┘
484  ⟨uniform_space.of_core { uniformity := ⊤, refl := le_top, symm := le_top, comp := le_top }⟩
id    └───────────────────┘                           └────┘          └────┘          └────┘
src   └───────────────────┘                           └────┘          └────┘          └────┘
typ   └───────────────────┘                           └────┘          └────┘          └────┘
485  
486  instance : has_bot (uniform_space α) :=
id              └─────┘  └───────────┘ 
src             └─────┘  └───────────┘
typ             └─────┘  └───────────┘ 
doc             └─────┘  └───────────┘
487  ⟨{ to_topological_space := ⊥,
id                              
src                             
typ                             
488    uniformity  := principal id_rel,
id                    └───────┘ └────┘
src                   └───────┘ └────┘
typ                   └───────┘ └────┘
doc                   └───────┘ └────┘
489    refl        := le_refl _,
id                    └─────┘
src                   └─────┘
typ                   └─────┘
490    symm        := by simp [tendsto]; apply subset.refl,
id                             └─────┘
src                      └────┘└─────┘  └────┘
typ                      └────┘└─────┘  └────┘
doc                      └────┘└─────┘  └────┘
txt                      └────┘         └────┘
par                      └────┘         └────┘
pid                                        
st                      └────────────────────────────────┘
491    comp        :=
492    begin
st     └─────
493      rw [lift'_principal], {simp},
id           └─────────────┘
src      └──┘└─────────────┘   └──┘
typ      └──┘└─────────────┘   └──┘
doc      └──┘                  └──┘
txt      └──┘                  └──┘
par      └──┘                  └──┘
pid        └┘               
st   ──────────────────────┘└──────┘└┘
494      exact monotone_comp_rel monotone_id monotone_id
id             └───────────────┘             └─────────┘
src      └────┘└───────────────┘           └─────────┘
typ      └────┘└───────────────┘           └─────────┘
doc      └────┘                                       
txt      └────┘                                       
par      └────┘                                       
pid                                                  
st   ────────────────────────────────────────────────────
495    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
496    is_open_uniformity :=
497      assume s, by simp [is_open_fold, subset_def, id_rel] {contextual := tt } } ⟩
id                         └──────────┘  └────────┘  └────┘                 └┘
src                   └────┘└──────────┘└┘└────────┘└┘└────┘└┘ └────────────┘└┘└─┘
typ                  └────┘└──────────┘└┘└────────┘└┘└────┘└┘ └────────────┘└┘└─┘
doc                   └────┘            └┘          └┘└────┘└┘ └────────────┘  └─┘
txt                   └────┘            └┘          └┘      └┘ └────────────┘  └─┘
par                   └────┘            └┘          └┘      └┘ └────────────┘  └─┘
pid                                   └┘          └┘       └────────────┘  └┘
st                   └───────────────────────────────────────────────────────────┘
498  
499  instance : complete_lattice (uniform_space α) :=
id              └──────────────┘  └───────────┘ 
src             └──────────────┘  └───────────┘
typ             └──────────────┘  └───────────┘ 
doc             └──────────────┘  └───────────┘
500  { sup           := λa b, Inf {x | a ≤ x ∧ b ≤ x},
id                          └─┘          
src                           └─┘             
typ                         └─┘          
doc                           └─┘
501    le_sup_left   := λ a b, le_Inf (λ _ ⟨h, _⟩, h),
id                           └────┘     
src                            └────┘
typ                          └────┘     
502    le_sup_right  := λ a b, le_Inf (λ _ ⟨_, h⟩, h),
id                           └────┘        
src                            └────┘
typ                          └────┘        
503    sup_le        := λ a b c h₁ h₂, Inf_le ⟨h₁, h₂⟩,
id                           └┘ └┘  └────┘  └┘  └┘
src                                    └────┘
typ                          └┘ └┘  └────┘  └┘  └┘
504    inf           := λ a b, Inf {a, b},
id                           └─┘  
src                            └─┘  
typ                          └─┘  
doc                            └─┘
505    le_inf        := λ a b c h₁ h₂, le_Inf (λ u h,
id                           └┘ └┘  └────┘     
src                                    └────┘
typ                          └┘ └┘  └────┘     
506                       by { cases h, exact h.symm ▸ h₂, exact (mem_singleton_iff.1 h).symm ▸ h₁ }),
id                                           └────┘  └┘         └───────────────┘            └┘
src                            └────┘   └────┘└────┘    └────┘ └───────────────┘└─┘ └─────┘   
typ                            └────┘  └────┘└────┘└┘  └────┘ └───────────────┘└─┘└─────┘ └┘
doc                            └────┘   └────┘           └────┘                  └─┘ └─────┘   
txt                            └────┘   └────┘           └────┘                  └─┘ └─────┘   
par                            └────┘   └────┘           └────┘                  └─┘ └─────┘   
pid                                                                           └─┘ └─────┘   
st                          └────────┘└─────────────────┘└────────────────────────────────────────┘└┘
507    inf_le_left   := λ a b, Inf_le (by simp),
id                           └────┘
src                            └────┘     └──┘
typ                          └────┘     └──┘
doc                                       └──┘
txt                                       └──┘
par                                       └──┘
st                                       └───┘
508    inf_le_right  := λ a b, Inf_le (by simp),
id                           └────┘
src                            └────┘     └──┘
typ                          └────┘     └──┘
doc                                       └──┘
txt                                       └──┘
par                                       └──┘
st                                       └───┘
509    top           := ⊤,
id                      
src                     
typ                     
510    le_top        := λ a, show a.uniformity ≤ ⊤, from le_top,
id                               └─────────┘         └────┘
src                                └─────────┘         └────┘
typ                              └─────────┘         └────┘
511    bot           := ⊥,
id                      
src                     
typ                     
512    bot_le        := λ u, u.refl,
id                          └───┘
src                           └───┘
typ                         └───┘
513    Sup           := λ tt, Inf {t | ∀ t' ∈ tt, t' ≤ t},
id                        └┘  └─┘      └┘   └┘  └┘  
src                           └─┘                   
typ                       └┘  └─┘      └┘   └┘  └┘  
doc                           └─┘
514    le_Sup        := λ s u h, le_Inf (λ u' h', h' u h),
id                            └────┘    └┘ └┘  └┘  
src                              └────┘
typ                           └────┘    └┘ └┘  └┘  
515    Sup_le        := λ s u h, Inf_le h,
id                            └────┘ 
src                              └────┘
typ                           └────┘ 
516    Inf           := Inf,
id                      └─┘
src                     └─┘
typ                     └─┘
doc                     └─┘
517    le_Inf        := λ s a hs, le_Inf hs,
id                          └┘  └────┘ └┘
src                               └────┘
typ                         └┘  └────┘ └┘
518    Inf_le        := λ s a ha, Inf_le ha,
id                          └┘  └────┘ └┘
src                               └────┘
typ                         └┘  └────┘ └┘
519    ..uniform_space.partial_order }
id       └─────────────────────────┘
src      └─────────────────────────┘
typ      └─────────────────────────┘
520  
521  lemma infi_uniformity {ι : Sort*} {u : ι → uniform_space α} :
id                                             └───────────┘ 
src                                             └───────────┘
typ                                            └───────────┘ 
doc                                             └───────────┘
522    (infi u).uniformity = (⨅i, (u i).uniformity) :=
id      └──┘  └────────┘        └────────┘
src     └──┘   └────────┘           └────────┘
typ     └──┘  └────────┘        └────────┘
doc     └──┘                   
523  show (⨅a (h : ∃i:ι, u i = a), a.uniformity) = _, from
id                       └─────────┘  
src                            └─────────┘  
typ                      └─────────┘  
doc                             
524  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
525    (le_infi $ assume i, infi_le_of_le (u i) $ infi_le _ ⟨i, rfl⟩)
id      └─────┘            └───────────┘       └─────┘      └─┘
src     └─────┘             └───────────┘         └─────┘       └─┘
typ     └─────┘            └───────────┘       └─────┘      └─┘
526    (le_infi $ assume a, le_infi $ assume ⟨i, (ha : u i = a)⟩, ha ▸ infi_le _ _)
id      └─────┘            └─────┘                              └─────┘
src     └─────┘             └─────┘                                  └─────┘
typ     └─────┘            └─────┘                              └─────┘
527  
528  lemma inf_uniformity {u v : uniform_space α} :
id                               └───────────┘ 
src                              └───────────┘
typ                              └───────────┘ 
doc                              └───────────┘
529    (u ⊓ v).uniformity = u.uniformity ⊓ v.uniformity :=
id         └────────┘   └─────────┘  └─────────┘
src          └────────┘    └─────────┘   └─────────┘
typ        └────────┘   └─────────┘  └─────────┘
530  have (u ⊓ v) = (⨅i (h : i = u ∨ i = v), i), by simp [infi_or, infi_inf_eq],
id                                         └─────┘  └─────────┘
src                                          └────┘└─────┘└┘└─────────┘
typ                                  └────┘└─────┘└┘└─────────┘
doc                                               └────┘       └┘           
txt                                                 └────┘       └┘           
par                                                 └────┘       └┘           
pid                                                            └┘           
st                                                 └──────────────────────────┘
531  calc (u ⊓ v).uniformity = ((⨅i (h : i = u ∨ i = v), i) : uniform_space α).uniformity : by rw [this]
id            └────────┘                        └───────────┘  └────────┘           └──┘
src             └────────┘                              └───────────┘   └────────┘       └──┘    └─
typ           └────────┘                        └───────────┘  └────────┘       └──┘└──┘└─
doc                                                         └───────────┘                    └──┘    └─
txt                                                                                            └──┘    └─
par                                                                                            └──┘    └─
pid                                                                                              └┘    
st                                                                                            └───────┘
532    ... = _ : by simp [infi_uniformity, infi_or, infi_inf_eq]
id                        └─────────────┘  └─────┘  └─────────┘
src  ─┘             └────┘└─────────────┘└┘└─────┘└┘└─────────┘└─
typ  ─┘             └────┘└─────────────┘└┘└─────┘└┘└─────────┘└─
doc  ─┘             └────┘               └┘       └┘           └─
txt  ─┘             └────┘               └┘       └┘           └─
par  ─┘             └────┘               └┘       └┘           └─
pid  ─┘                                └┘       └┘           
st   ─┘            └─────────────────────────────────────────────
533  
src  
typ  
doc  
txt  
par  
pid  
st   
534  instance inhabited_uniform_space : inhabited (uniform_space α) := ⟨⊥⟩
id                                      └───────┘  └───────────┘       
src                                     └───────┘  └───────────┘        
typ                                     └───────┘  └───────────┘       
doc                                                └───────────┘
535  instance inhabited_uniform_space_core : inhabited (uniform_space.core α) :=
id                                           └───────┘  └────────────────┘ 
src                                          └───────┘  └────────────────┘
typ                                          └───────┘  └────────────────┘ 
doc                                                     └────────────────┘
536  ⟨@uniform_space.to_core _ (default _)⟩
id     └───────────────────┘    └─────┘
src    └───────────────────┘    └─────┘
typ    └───────────────────┘    └─────┘
537  
538  /-- Given `f : α → β` and a uniformity `u` on `β`, the inverse image of `u` under `f`
539    is the inverse image in the filter sense of the induced function `α × α → β × β`. -/
540  def uniform_space.comap (f : α → β) (u : uniform_space β) : uniform_space α :=
id                                          └───────────┘     └───────────┘ 
src                                           └───────────┘      └───────────┘
typ                                         └───────────┘     └───────────┘ 
doc                                           └───────────┘      └───────────┘
541  { uniformity := u.uniformity.comap (λp:α×α, (f p.1, f p.2)),
id                   └─────────┘└────┘            
src                   └─────────┘└────┘                  
typ                  └─────────┘└────┘            
doc                              └────┘
542    to_topological_space := u.to_topological_space.induced f,
id                             └───────────────────┘└──────┘ 
src                             └───────────────────┘└──────┘
typ                            └───────────────────┘└──────┘ 
doc                                                  └──────┘
543    refl := le_trans (by simp; exact assume ⟨a, b⟩ (h : a = b), h ▸ rfl) (comap_mono u.refl),
id             └──────┘                                                      └────────┘ └───┘
src            └──────┘     └──┘  └────┘      └┘ └┘ └─────┘   └─┘        └────────┘  └───┘
typ            └──────┘     └──┘  └────┘      └┘ └┘ └─────┘   └─┘        └────────┘ └───┘
doc                         └──┘  └────┘      └┘ └┘ └─────┘   └─┘  
txt                         └──┘  └────┘      └┘ └┘ └─────┘   └─┘  
par                         └──┘  └────┘      └┘ └┘ └─────┘   └─┘  
pid                                          └┘ └┘ └─────┘   └─┘  
st                         └─────────────────────────────────────────────┘
544    symm := by simp [tendsto_comap_iff, prod.swap, (∘)]; exact tendsto_swap_uniformity.comp tendsto_comap,
id                      └───────────────┘  └───────┘             └──────────────────────────┘ └───────────┘
src               └────┘└───────────────┘└┘└───────┘└┘└─┘  └────┘└──────────────────────────┘└───────────┘
typ               └────┘└───────────────┘└┘└───────┘└┘└─┘  └────┘└──────────────────────────┘└───────────┘
doc               └────┘                 └┘└───────┘└┘ └─┘  └────┘                            
txt               └────┘                 └┘         └┘ └─┘  └────┘                            
par               └────┘                 └┘         └┘ └─┘  └────┘                            
pid                                    └┘         └┘ └─┘                                   
st               └─────────────────────────────────────────────────────────────────────────────────────────┘
545    comp := le_trans
id             └──────┘
src            └──────┘
typ            └──────┘
546      begin
st       └─────
547        rw [comap_lift'_eq, comap_lift'_eq2],
id             └────────────┘  └─────────────┘
src        └──┘└────────────┘└┘└─────────────┘
typ        └──┘└────────────┘└┘└─────────────┘
doc        └──┘              └┘               
txt        └──┘              └┘               
par        └──┘              └┘               
pid          └┘              └┘               
st   ───────────────────────┘└───────────────┘└──
548        exact (lift'_mono' $ assume s hs ⟨a₁, a₂⟩ ⟨x, h₁, h₂⟩, ⟨f x, h₁, h₂⟩),
id                └─────────┘                           └┘  └┘    
src        └────┘ └─────────┘       └─────┘  └┘  └─┘ └┘  └┘  └─┘   └┘  └┘  └┘
typ        └────┘ └─────────┘       └─────┘  └┘  └─┘└┘└┘└┘└┘└─┘  └┘  └┘  └┘
doc        └────┘                   └─────┘  └┘  └─┘ └┘  └┘  └─┘   └┘  └┘  └┘
txt        └────┘                   └─────┘  └┘  └─┘ └┘  └┘  └─┘   └┘  └┘  └┘
par        └────┘                   └─────┘  └┘  └─┘ └┘  └┘  └─┘   └┘  └┘  └┘
pid                                └─────┘  └┘  └─┘ └┘  └┘  └─┘   └┘  └┘  └┘
st   ──────────────────────────────────────────────────────────────────────────┘└─
549        repeat { exact monotone_comp_rel monotone_id monotone_id }
id                        └───────────────┘             └─────────┘
src        └───────┘└────┘└───────────────┘           └─────────┘└─
typ        └───────┘└────┘└───────────────┘           └─────────┘└─
doc        └───────┘└────┘                                       └─
txt        └───────┘└────┘                                       └─
par        └───────┘└────┘                                       └─
pid              └───────┘                                       └┘
st   ─────────────┘└───────────────────────────────────────────────┘
550      end
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
551      (comap_mono u.comp),
id        └────────┘ └───┘
src       └────────┘  └───┘
typ       └────────┘ └───┘
552    is_open_uniformity := λ s, begin
id                             
typ                            
st                                └─────
553      change (@is_open α (u.to_topological_space.induced f) s ↔ _),
id                └─────┘   └────────────────────────────┘   
src      └─────┘  └─────┘  └────────────────────────────┘ └┘  └─┘
typ      └─────┘  └─────┘ └────────────────────────────┘└┘ └─┘
doc      └─────┘  └─────┘  └────────────────────────────┘ └┘  └─┘
txt      └─────┘                                          └┘  └─┘
par      └─────┘                                          └┘  └─┘
pid                                                      └┘  └─┘
st   ───────────────────────────────────────────────────────────────┘└─
554      simp [is_open_iff_nhds, nhds_induced, mem_nhds_uniformity_iff, filter.comap, and_comm],
id             └──────────────┘  └──────────┘  └─────────────────────┘  └──────────┘  └──────┘
src      └────┘└──────────────┘└┘└──────────┘└┘└─────────────────────┘└┘└──────────┘└┘└──────┘
typ      └────┘└──────────────┘└┘└──────────┘└┘└─────────────────────┘└┘└──────────┘└┘└──────┘
doc      └────┘                └┘            └┘                       └┘└──────────┘└┘        
txt      └────┘                └┘            └┘                       └┘            └┘        
par      └────┘                └┘            └┘                       └┘            └┘        
pid                          └┘            └┘                       └┘            └┘        
st   ─────────────────────────────────────────────────────────────────────────────────────────┘└─
555      refine ball_congr (λ x hx, ⟨_, _⟩),
id              └────────┘
src      └─────┘└────────┘  └─────┘ └────┘
typ      └─────┘└────────┘  └─────┘ └────┘
doc      └─────┘            └─────┘ └────┘
txt      └─────┘            └─────┘ └────┘
par      └─────┘            └─────┘ └────┘
pid                        └─────┘ └────┘
st   ─────────────────────────────────────┘└─
556      { rintro ⟨t, hts, ht⟩, refine ⟨_, ht, _⟩,
id                                         └┘
src        └─────────────────┘  └─────┘ └─┘  └──┘
typ        └─────────────────┘  └─────┘ └─┘└┘└──┘
doc        └─────────────────┘  └─────┘ └─┘  └──┘
txt        └─────────────────┘  └─────┘ └─┘  └──┘
par        └─────────────────┘  └─────┘ └─┘  └──┘
pid              └───────────┘         └─┘  └──┘
st   ─────┘└─────────────────┘└─────────────────┘└─
557        rintro ⟨x₁, x₂⟩ h rfl, exact hts (h rfl) },
id                                      └─┘   └─┘
src        └───────────────────┘  └────┘     └─┘└┘
typ        └───────────────────┘  └────┘└─┘ └─┘└┘
doc        └───────────────────┘  └────┘        └┘
txt        └───────────────────┘  └────┘        └┘
par        └───────────────────┘  └────┘        └┘
pid              └─────────────┘               
st   ──────────────────────────┘└──────────────────┘└┘
558      { rintro ⟨t, ht, hts⟩,
src        └─────────────────┘
typ        └─────────────────┘
doc        └─────────────────┘
txt        └─────────────────┘
par        └─────────────────┘
pid              └───────────┘
st   ────────────────────────┘└─
559        exact ⟨{y | (f x, y) ∈ t}, λ y hy, @hts (x, y) hy rfl,
id                                        └─┘          └─┘
src        └────┘ └──┘  └┘ └┘ └─┘ └─────┘      └┘ └┘  └─┘└─
typ        └────┘ └──┘ └┘ └┘└─┘ └─────┘ └─┘ └┘ └┘  └─┘└─
doc        └────┘  └──┘   └┘ └┘  └─┘ └─────┘      └┘ └┘     └─
txt        └────┘  └──┘   └┘ └┘  └─┘ └─────┘      └┘ └┘     └─
par        └────┘  └──┘   └┘ └┘  └─┘ └─────┘      └┘ └┘     └─
pid               └──┘   └┘ └┘  └─┘ └─────┘      └┘ └┘     └─
st   ─────────────────────────────────────────────────────────────
560          mem_nhds_uniformity_iff.1 $ mem_nhds_left _ ht⟩ }
id           └─────────────────────┘     └───────────┘   └┘
src  ───────┘└─────────────────────┘└─┘ └───────────┘└─┘  └┘
typ  ───────┘└─────────────────────┘└─┘ └───────────┘└─┘└┘└┘
doc  ───────┘                       └─┘              └─┘  └┘
txt  ───────┘                       └─┘              └─┘  └┘
par  ───────┘                       └─┘              └─┘  └┘
pid  ───────┘                       └─┘              └─┘  
st   ───────────────────────────────────────────────────────┘└─
561    end }
st   ────┘
562  
563  lemma uniform_space_comap_id {α : Type*} : uniform_space.comap (id : α → α) = id :=
id                                              └─────────────────┘  └┘         └┘
src                                             └─────────────────┘  └┘           └┘
typ                                             └─────────────────┘  └┘         └┘
doc                                             └─────────────────┘
564  by ext u ; dsimp [uniform_space.comap] ; rw [prod.id_prod, filter.comap_id]
id                     └─────────────────┘        └──────────┘  └─────────────┘
src     └────┘  └─────┘└─────────────────┘└┘  └──┘└──────────┘└┘└─────────────┘└─
typ     └────┘  └─────┘└─────────────────┘└┘  └──┘└──────────┘└┘└─────────────┘└─
doc     └────┘  └─────┘└─────────────────┘└┘  └──┘            └┘               └─
txt     └────┘  └─────┘                   └┘  └──┘            └┘               └─
par     └────┘  └─────┘                   └┘  └──┘            └┘               └─
pid        └┘                              └┘            └┘               
st     └─────────────────────────────────────────┘└──────────┘└───────────────┘
565  
src  
typ  
doc  
txt  
par  
pid  
st   
566  lemma uniform_space.comap_comap_comp {α β γ} [uγ : uniform_space γ] {f : α → β} {g : β → γ} :
id                                                      └───────────┘                     
src                                                     └───────────┘
typ                                                     └───────────┘                     
doc                                                     └───────────┘
567    uniform_space.comap (g ∘ f) uγ = uniform_space.comap f (uniform_space.comap g uγ) :=
id     └─────────────────┘      └┘  └─────────────────┘   └─────────────────┘  └┘
src    └─────────────────┘            └─────────────────┘    └─────────────────┘
typ    └─────────────────┘      └┘  └─────────────────┘   └─────────────────┘  └┘
doc    └─────────────────┘              └─────────────────┘    └─────────────────┘
568  by ext ; dsimp [uniform_space.comap] ; rw filter.comap_comap_comp
id                   └─────────────────┘       └─────────────────────┘
src     └──┘  └─────┘└─────────────────┘└┘  └─┘└─────────────────────┘
typ     └──┘  └─────┘└─────────────────┘└┘  └─┘└─────────────────────┘
doc     └──┘  └─────┘└─────────────────┘└┘  └─┘                       
txt     └──┘  └─────┘                   └┘  └─┘                       
par     └──┘  └─────┘                   └┘  └─┘                       
pid                                                             
st     └──────────────────────────────────────┘└─────────────────────┘
569  
src  
typ  
doc  
txt  
par  
pid  
st   
570  lemma uniform_continuous_iff {α β} [uα : uniform_space α] [uβ : uniform_space β] {f : α → β} :
id                                            └───────────┘         └───────────┘           
src                                           └───────────┘          └───────────┘
typ                                           └───────────┘         └───────────┘           
doc                                           └───────────┘          └───────────┘
571    uniform_continuous f ↔ uα ≤ uβ.comap f :=
id     └────────────────┘   └┘  └┘└────┘ 
src    └────────────────┘          └────┘
typ    └────────────────┘   └┘  └┘└────┘ 
doc                                  └────┘
572  filter.map_le_iff_le_comap
id   └────────────────────────┘
src  └────────────────────────┘
typ  └────────────────────────┘
573  
574  lemma uniform_continuous_comap {f : α → β} [u : uniform_space β] :
id                                                 └───────────┘ 
src                                                  └───────────┘
typ                                                └───────────┘ 
doc                                                  └───────────┘
575    @uniform_continuous α β (uniform_space.comap f u) u f :=
id      └────────────────┘    └─────────────────┘     
src     └────────────────┘      └─────────────────┘
typ     └────────────────┘    └─────────────────┘     
doc                             └─────────────────┘
576  tendsto_comap
id   └───────────┘
src  └───────────┘
typ  └───────────┘
577  
578  theorem to_topological_space_comap {f : α → β} {u : uniform_space β} :
id                                                     └───────────┘ 
src                                                      └───────────┘
typ                                                    └───────────┘ 
doc                                                      └───────────┘
579    @uniform_space.to_topological_space _ (uniform_space.comap f u) =
id      └────────────────────────────────┘    └─────────────────┘    
src     └────────────────────────────────┘    └─────────────────┘      
typ     └────────────────────────────────┘    └─────────────────┘    
doc                                           └─────────────────┘
580    topological_space.induced f (@uniform_space.to_topological_space β u) := rfl
id     └───────────────────────┘    └────────────────────────────────┘       └─┘
src    └───────────────────────┘     └────────────────────────────────┘         └─┘
typ    └───────────────────────┘    └────────────────────────────────┘       └─┘
doc    └───────────────────────┘
581  
582  lemma uniform_continuous_comap' {f : γ → β} {g : α → γ} [v : uniform_space β] [u : uniform_space α]
id                                                            └───────────┘        └───────────┘ 
src                                                               └───────────┘         └───────────┘
typ                                                           └───────────┘        └───────────┘ 
doc                                                               └───────────┘         └───────────┘
583    (h : uniform_continuous (f ∘ g)) : @uniform_continuous α γ u (uniform_space.comap f v) g :=
id          └────────────────┘          └────────────────┘     └─────────────────┘    
src         └────────────────┘            └────────────────┘        └─────────────────┘
typ         └────────────────┘          └────────────────┘     └─────────────────┘    
doc                                                                  └─────────────────┘
584  tendsto_comap_iff.2 h
id   └───────────────┘  
src  └───────────────┘
typ  └───────────────┘  
585  
586  lemma to_topological_space_mono {u₁ u₂ : uniform_space α} (h : u₁ ≤ u₂) :
id                                            └───────────┘        └┘  └┘
src                                           └───────────┘            
typ                                           └───────────┘        └┘  └┘
doc                                           └───────────┘
587    @uniform_space.to_topological_space _ u₁ ≤ @uniform_space.to_topological_space _ u₂ :=
id      └────────────────────────────────┘   └┘   └────────────────────────────────┘   └┘
src     └────────────────────────────────┘        └────────────────────────────────┘
typ     └────────────────────────────────┘   └┘   └────────────────────────────────┘   └┘
588  le_of_nhds_le_nhds $ assume a,
id   └────────────────┘          
src  └────────────────┘
typ  └────────────────┘          
589    by rw [@nhds_eq_uniformity α u₁ a, @nhds_eq_uniformity α u₂ a]; exact (lift'_mono h $ le_refl _)
id             └────────────────┘  └┘    └────────────────┘  └┘           └────────┘    └─────┘
src       └──┘ └────────────────┘    └┘ └────────────────┘      └────┘ └────────┘  └─────┘└───
typ       └──┘ └────────────────┘└┘└┘ └────────────────┘└┘  └────┘ └────────┘ └─────┘└───
doc       └──┘                       └┘                         └────┘                    └───
txt       └──┘                       └┘                         └────┘                    └───
par       └──┘                       └┘                         └────┘                    └───
pid         └┘                       └┘                                                  └─┘
st       └─────────────────────────────┘└──────────────────────────┘└──────────────────────────────────
590  
src  
typ  
doc  
txt  
par  
pid  
st   
591  lemma uniform_continuous.continuous [uniform_space α] [uniform_space β] {f : α → β}
id                                        └───────────┘    └───────────┘           
src                                       └───────────┘     └───────────┘
typ                                       └───────────┘    └───────────┘           
doc                                       └───────────┘     └───────────┘
592    (hf : uniform_continuous f) : continuous f :=
id           └────────────────┘     └────────┘ 
src          └────────────────┘      └────────┘
typ          └────────────────┘     └────────┘ 
doc                                  └────────┘
593  continuous_iff_le_induced.mpr $ to_topological_space_mono $ uniform_continuous_iff.1 hf
id   └───────────────────────┘└──┘   └───────────────────────┘   └────────────────────┘  └┘
src  └───────────────────────┘└──┘   └───────────────────────┘   └────────────────────┘
typ  └───────────────────────┘└──┘   └───────────────────────┘   └────────────────────┘  └┘
594  
595  lemma to_topological_space_bot : @uniform_space.to_topological_space α ⊥ = ⊥ := rfl
id                                     └────────────────────────────────┘        └─┘
src                                    └────────────────────────────────┘         └─┘
typ                                    └────────────────────────────────┘        └─┘
596  
597  lemma to_topological_space_top : @uniform_space.to_topological_space α ⊤ = ⊤ :=
id                                     └────────────────────────────────┘    
src                                    └────────────────────────────────┘     
typ                                    └────────────────────────────────┘    
598  top_unique $ assume s hs, s.eq_empty_or_nonempty.elim
id   └────────┘           └┘  └───────────────────┘└───┘
src  └────────┘                 └───────────────────┘└───┘
typ  └────────┘           └┘  └───────────────────┘└───┘
599    (assume : s = ∅, this.symm ▸ @is_open_empty _ ⊤)
id                   └──┘└───┘   └───────────┘   
src                       └───┘   └───────────┘   
typ                  └──┘└───┘   └───────────┘   
600    (assume  ⟨x, hx⟩,
id                └┘
typ               └┘
601      have s = univ, from top_unique $ assume y hy, hs x hx (x, y) rfl,
id              └──┘       └────────┘           └┘  └┘           └─┘
src              └──┘       └────────┘                              └─┘
typ             └──┘       └────────┘           └┘  └┘           └─┘
602      this.symm ▸ @is_open_univ _ ⊤)
id       └──┘└───┘   └──────────┘   
src          └───┘   └──────────┘   
typ      └──┘└───┘   └──────────┘   
603  
604  lemma to_topological_space_infi {ι : Sort*} {u : ι → uniform_space α} :
id                                                       └───────────┘ 
src                                                       └───────────┘
typ                                                      └───────────┘ 
doc                                                       └───────────┘
605    (infi u).to_topological_space = ⨅i, (u i).to_topological_space :=
id      └──┘  └──────────────────┘       └──────────────────┘
src     └──┘   └──────────────────┘          └──────────────────┘
typ     └──┘  └──────────────────┘       └──────────────────┘
doc     └──┘                            
606  classical.by_cases
id   └────────────────┘
src  └────────────────┘
typ  └────────────────┘
607    (assume h : nonempty ι,
id                 └──────┘ 
src                └──────┘
typ                └──────┘ 
608      eq_of_nhds_eq_nhds $ assume a,
id       └────────────────┘          
src      └────────────────┘
typ      └────────────────┘          
609      begin
st       └─────
610        rw [nhds_infi, nhds_eq_uniformity],
id             └───────┘  └────────────────┘
src        └──┘└───────┘└┘└────────────────┘
typ        └──┘└───────┘└┘└────────────────┘
doc        └──┘         └┘                  
txt        └──┘         └┘                  
par        └──┘         └┘                  
pid          └┘         └┘                  
st   ──────────────────┘└──────────────────┘└──
611        change (infi u).uniformity.lift' (preimage $ prod.mk a) = _,
id                 └──┘                     └──────┘   └─────┘   
src        └─────┘ └──┘ └─────────────────┘ └──────┘ └─────┘ └┘└┘
typ        └─────┘ └──┘└─────────────────┘ └──────┘ └─────┘└┘└┘
doc        └─────┘ └──┘ └─────────────────┘ └──────┘         └┘ └┘
txt        └─────┘      └─────────────────┘                  └┘ └┘
par        └─────┘      └─────────────────┘                  └┘ └┘
pid                    └─────────────────┘                  └┘ └┘
st   ────────────────────────────────────────────────────────────────┘└─
612        begin
st   ────────────
613          rw [infi_uniformity, lift'_infi],
id               └─────────────┘  └────────┘
src          └──┘└─────────────┘└┘└────────┘
typ          └──┘└─────────────┘└┘└────────┘
doc          └──┘               └┘          
txt          └──┘               └┘          
par          └──┘               └┘          
pid            └┘               └┘          
st   ──────────────────────────┘└──────────┘└──
614          exact (congr_arg _ $ funext $ assume i, (@nhds_eq_uniformity α (u i) a).symm),
id                  └───────┘     └────┘               └────────────────┘       
src          └────┘ └───────┘└─┘ └────┘       └──┘  └────────────────┘    └┘ └─────┘
typ          └────┘ └───────┘└─┘ └────┘       └──┘  └────────────────┘  └┘└─────┘
doc          └────┘          └─┘              └──┘                        └┘ └─────┘
txt          └────┘          └─┘              └──┘                        └┘ └─────┘
par          └────┘          └─┘              └──┘                        └┘ └─────┘
pid                         └─┘              └──┘                        └┘ └─────┘
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
615          exact h,
id                 
src          └────┘
typ          └────┘
doc          └────┘
txt          └────┘
par          └────┘
pid               
st   ──────────────┘└─
616          exact assume a b, rfl
id                             └─┘
src          └────┘      └────┘└─┘
typ          └────┘      └────┘└─┘
doc          └────┘      └────┘   
txt          └────┘      └────┘   
par          └────┘      └────┘   
pid                     └────┘   
st   ──────────────────────────────
617        end
src  ─────┘
typ  ─────┘
doc  ─────┘
txt  ─────┘
par  ─────┘
pid  ─────┘
st   ─────┘└───
618      end)
st   ──────┘
619    (assume : ¬ nonempty ι,
id                └──────┘ 
src               └──────┘
typ               └──────┘ 
620      le_antisymm
id       └─────────┘
src      └─────────┘
typ      └─────────┘
621        (le_infi $ assume i, to_topological_space_mono $ infi_le _ _)
id          └─────┘            └───────────────────────┘   └─────┘
src         └─────┘             └───────────────────────┘   └─────┘
typ         └─────┘            └───────────────────────┘   └─────┘
622        (have infi u = ⊤, from top_unique $ le_infi $ assume i, (this ⟨i⟩).elim,
id               └──┘          └────────┘   └─────┘             └──┘    └──┘
src              └──┘           └────────┘   └─────┘                       └──┘
typ              └──┘          └────────┘   └─────┘             └──┘    └──┘
doc              └──┘
623          have @uniform_space.to_topological_space _ (infi u) = ⊤,
id                 └────────────────────────────────┘    └──┘    
src                └────────────────────────────────┘    └──┘     
typ                └────────────────────────────────┘    └──┘    
doc                                                      └──┘
624            from this.symm ▸ to_topological_space_top,
id                  └──┘└───┘  └──────────────────────┘
src                     └───┘  └──────────────────────┘
typ                 └──┘└───┘  └──────────────────────┘
625          this.symm ▸ le_top))
id           └──┘└───┘  └────┘
src              └───┘  └────┘
typ          └──┘└───┘  └────┘
626  
627  lemma to_topological_space_Inf {s : set (uniform_space α)} :
id                                       └─┘  └───────────┘ 
src                                      └─┘  └───────────┘
typ                                      └─┘  └───────────┘ 
doc                                           └───────────┘
628    (Inf s).to_topological_space = (⨅i∈s, @uniform_space.to_topological_space α i) :=
id      └─┘  └──────────────────┘       └────────────────────────────────┘  
src     └─┘   └──────────────────┘         └────────────────────────────────┘
typ     └─┘  └──────────────────┘       └────────────────────────────────┘  
doc     └─┘                               
629  begin
st   └─────
630    rw [Inf_eq_infi, to_topological_space_infi],
id         └─────────┘  └───────────────────────┘
src    └──┘└─────────┘└┘└───────────────────────┘
typ    └──┘└─────────┘└┘└───────────────────────┘
doc    └──┘           └┘                         
txt    └──┘           └┘                         
par    └──┘           └┘                         
pid      └┘           └┘                         
st   ────────────────┘└─────────────────────────┘└──
631    apply congr rfl,
id           └───┘ └─┘
src    └────┘└───┘└─┘
typ    └────┘└───┘└─┘
doc    └────┘     
txt    └────┘     
par    └────┘     
pid              
st   ────────────────┘└─
632    funext x,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid          └┘
st   ─────────┘└─
633    exact to_topological_space_infi
id           └───────────────────────┘
src    └────┘└───────────────────────┘
typ    └────┘└───────────────────────┘
doc    └────┘                         
txt    └────┘                         
par    └────┘                         
pid                                  
st   ─────────────────────────────────┘
634  end
st   └─┘
635  
636  lemma to_topological_space_inf {u v : uniform_space α} :
id                                         └───────────┘ 
src                                        └───────────┘
typ                                        └───────────┘ 
doc                                        └───────────┘
637    (u ⊓ v).to_topological_space = u.to_topological_space ⊓ v.to_topological_space :=
id         └──────────────────┘   └───────────────────┘  └───────────────────┘
src          └──────────────────┘    └───────────────────┘   └───────────────────┘
typ        └──────────────────┘   └───────────────────┘  └───────────────────┘
638  by rw [to_topological_space_Inf, infi_pair]
id          └──────────────────────┘  └───────┘
src     └──┘└──────────────────────┘└┘└───────┘└─
typ     └──┘└──────────────────────┘└┘└───────┘└─
doc     └──┘                        └┘         └─
txt     └──┘                        └┘         └─
par     └──┘                        └┘         └─
pid       └┘                        └┘         
st     └───────────────────────────┘└─────────┘
639  
src  
typ  
doc  
txt  
par  
pid  
st   
640  instance : uniform_space empty := ⊥
id              └───────────┘ └───┘    
src             └───────────┘ └───┘    
typ             └───────────┘ └───┘    
doc             └───────────┘
641  instance : uniform_space unit := ⊥
id              └───────────┘ └──┘    
src             └───────────┘ └──┘    
typ             └───────────┘ └──┘    
doc             └───────────┘ └──┘
642  instance : uniform_space bool := ⊥
id              └───────────┘ └──┘    
src             └───────────┘ └──┘    
typ             └───────────┘ └──┘    
doc             └───────────┘
643  instance : uniform_space ℕ := ⊥
id              └───────────┘     
src             └───────────┘     
typ             └───────────┘     
doc             └───────────┘
644  instance : uniform_space ℤ := ⊥
id              └───────────┘     
src             └───────────┘     
typ             └───────────┘     
doc             └───────────┘
645  
646  instance {p : α → Prop} [t : uniform_space α] : uniform_space (subtype p) :=
id                               └───────────┘     └───────────┘  └─────┘ 
src                               └───────────┘      └───────────┘  └─────┘
typ                              └───────────┘     └───────────┘  └─────┘ 
doc                               └───────────┘      └───────────┘
647  uniform_space.comap subtype.val t
id   └─────────────────┘ └─────────┘ 
src  └─────────────────┘ └─────────┘
typ  └─────────────────┘ └─────────┘ 
doc  └─────────────────┘
648  
649  lemma uniformity_subtype {p : α → Prop} [t : uniform_space α] :
id                                               └───────────┘ 
src                                               └───────────┘
typ                                              └───────────┘ 
doc                                               └───────────┘
650    𝓤 (subtype p) = comap (λq:subtype p × subtype p, (q.1.1, q.2.1)) (𝓤 α) :=
id       └─────┘    └───┘     └─────┘   └─────┘              
src      └─────┘     └───┘     └─────┘    └─────┘                
typ      └─────┘    └───┘     └─────┘   └─────┘              
doc                   └───┘                                             
651  rfl
id   └─┘
src  └─┘
typ  └─┘
652  
653  lemma uniform_continuous_subtype_val {p : α → Prop} [uniform_space α] :
id                                                       └───────────┘ 
src                                                       └───────────┘
typ                                                      └───────────┘ 
doc                                                       └───────────┘
654    uniform_continuous (subtype.val : {a : α // p a} → α) :=
id     └────────────────┘  └─────────┘                
src    └────────────────┘  └─────────┘   
typ    └────────────────┘  └─────────┘                
655  uniform_continuous_comap
id   └──────────────────────┘
src  └──────────────────────┘
typ  └──────────────────────┘
656  
657  lemma uniform_continuous_subtype_mk {p : α → Prop} [uniform_space α] [uniform_space β]
id                                                      └───────────┘    └───────────┘ 
src                                                      └───────────┘     └───────────┘
typ                                                     └───────────┘    └───────────┘ 
doc                                                      └───────────┘     └───────────┘
658    {f : β → α} (hf : uniform_continuous f) (h : ∀x, p (f x)) :
id                     └────────────────┘              
src                      └────────────────┘
typ                    └────────────────┘              
659    uniform_continuous (λx, ⟨f x, h x⟩ : β → subtype p) :=
id     └────────────────┘                 └─────┘ 
src    └────────────────┘                       └─────┘
typ    └────────────────┘                 └─────┘ 
660  uniform_continuous_comap' hf
id   └───────────────────────┘ └┘
src  └───────────────────────┘
typ  └───────────────────────┘ └┘
661  
662  lemma tendsto_of_uniform_continuous_subtype
663    [uniform_space α] [uniform_space β] {f : α → β} {s : set α} {a : α}
id      └───────────┘    └───────────┘                  └─┘        
src     └───────────┘     └───────────┘                     └─┘
typ     └───────────┘    └───────────┘                  └─┘        
doc     └───────────┘     └───────────┘
664    (hf : uniform_continuous (λx:s, f x.val)) (ha : s ∈ 𝓝 a) :
id           └────────────────┘        └──┘            
src          └────────────────┘           └──┘            
typ          └────────────────┘        └──┘            
doc                                                        
665    tendsto f (𝓝 a) (𝓝 (f a)) :=
id     └─────┘          
src    └─────┘         
typ    └─────┘          
doc    └─────┘         
666  by rw [(@map_nhds_subtype_val_eq α _ s a (mem_of_nhds ha) ha).symm]; exact
id            └─────────────────────┘       └─────────┘     └┘
src     └──┘  └─────────────────────┘ └─┘   └─────────┘  └┘  └─────┘  └────┘
typ     └──┘  └─────────────────────┘└─┘ └─────────┘  └┘└┘└─────┘  └────┘
doc     └──┘                          └─┘                └┘  └─────┘  └────┘
txt     └──┘                          └─┘                └┘  └─────┘  └────┘
par     └──┘                          └─┘                └┘  └─────┘  └────┘
pid       └┘                          └─┘                └┘  └─────┘       
st     └─────────────────────────────────────────────────────────────┘└┘└───────
667  tendsto_map' (continuous_iff_continuous_at.mp hf.continuous _)
id   └──────────┘  └─────────────────────────────┘ └───────────┘
src  └──────────┘ └─────────────────────────────┘└───────────┘└───
typ  └──────────┘ └─────────────────────────────┘└───────────┘└───
doc                                                           └───
txt                                                           └───
par                                                           └───
pid                                                           └─┘
st   ───────────────────────────────────────────────────────────────
668  
src  
typ  
doc  
txt  
par  
pid  
st   
669  
src  
typ  
doc  
txt  
par  
pid  
st   
670  section prod
671  
672  /- a similar product space is possible on the function space (uniformity of pointwise convergence),
673    but we want to have the uniformity of uniform convergence on function spaces -/
674  instance [u₁ : uniform_space α] [u₂ : uniform_space β] : uniform_space (α × β) :=
id                  └───────────┘         └───────────┘     └───────────┘    
src                 └───────────┘          └───────────┘      └───────────┘    
typ                 └───────────┘         └───────────┘     └───────────┘    
doc                 └───────────┘          └───────────┘      └───────────┘
675  uniform_space.of_core_eq
id   └──────────────────────┘
src  └──────────────────────┘
typ  └──────────────────────┘
676    (u₁.comap prod.fst ⊓ u₂.comap prod.snd).to_core
id      └┘└────┘ └──────┘  └┘└────┘ └──────┘ └─────┘
src       └────┘ └──────┘    └────┘ └──────┘ └─────┘
typ     └┘└────┘ └──────┘  └┘└────┘ └──────┘ └─────┘
doc       └────┘              └────┘
677    prod.topological_space
id     └────────────────────┘
src    └────────────────────┘
typ    └────────────────────┘
678    (calc prod.topological_space = (u₁.comap prod.fst ⊓ u₂.comap prod.snd).to_topological_space :
id           └────────────────────┘    └┘└────┘ └──────┘  └┘└────┘ └──────┘ └──────────────────┘
src          └────────────────────┘      └────┘ └──────┘    └────┘ └──────┘ └──────────────────┘
typ          └────────────────────┘    └┘└────┘ └──────┘  └┘└────┘ └──────┘ └──────────────────┘
doc                                      └────┘              └────┘
679        by rw [to_topological_space_inf, to_topological_space_comap, to_topological_space_comap]; refl
id                └──────────────────────┘  └────────────────────────┘  └────────────────────────┘
src           └──┘└──────────────────────┘└┘└────────────────────────┘└┘└────────────────────────┘  └────
typ           └──┘└──────────────────────┘└┘└────────────────────────┘└┘└────────────────────────┘  └────
doc           └──┘                        └┘                          └┘                            └────
txt           └──┘                        └┘                          └┘                            └────
par           └──┘                        └┘                          └┘                            └────
pid             └┘                        └┘                          └┘                                
st           └───────────────────────────┘└──────────────────────────┘└──────────────────────────┘└──────
680      ... = _ : by rw [uniform_space.to_core_to_topological_space])
id                        └────────────────────────────────────────┘
src  ───┘             └──┘└────────────────────────────────────────┘
typ  ───┘             └──┘└────────────────────────────────────────┘
doc  ───┘             └──┘                                          
txt  ───┘             └──┘                                          
par  ───┘             └──┘                                          
pid  ───┘               └┘                                          
st   ───┘            └─────────────────────────────────────────────┘
681  
682  theorem uniformity_prod [uniform_space α] [uniform_space β] : 𝓤 (α × β) =
id                            └───────────┘    └───────────┘           
src                           └───────────┘     └───────────┘              
typ                           └───────────┘    └───────────┘           
doc                           └───────────┘     └───────────┘      
683    (𝓤 α).comap (λp:(α × β) × α × β, (p.1.1, p.2.1)) ⊓
id        └───┘                         
src        └───┘                               
typ       └───┘                         
doc        └───┘
684    (𝓤 β).comap (λp:(α × β) × α × β, (p.1.2, p.2.2)) :=
id        └───┘                     
src        └───┘                           
typ       └───┘                     
doc        └───┘
685  inf_uniformity
id   └────────────┘
src  └────────────┘
typ  └────────────┘
686  
687  lemma uniformity_prod_eq_prod [uniform_space α] [uniform_space β] :
id                                  └───────────┘    └───────────┘ 
src                                 └───────────┘     └───────────┘
typ                                 └───────────┘    └───────────┘ 
doc                                 └───────────┘     └───────────┘
688    𝓤 (α×β) =
id         
src          
typ        
doc    
689      map (λp:(α×α)×(β×β), ((p.1.1, p.2.1), (p.1.2, p.2.2))) (filter.prod (𝓤 α) (𝓤 β)) :=
id       └─┘           └┘                    └─────────┘       
src      └─┘               └┘                        └─────────┘       
typ      └─┘                               └─────────┘       
doc      └─┘                                                     └─────────┘       
690  have map (λp:(α×α)×(β×β), ((p.1.1, p.2.1), (p.1.2, p.2.2))) =
id        └─┘           └┘                   
src       └─┘               └┘                       
typ       └─┘                              
doc       └─┘
691    comap (λp:(α×β)×(α×β), ((p.1.1, p.2.1), (p.1.2, p.2.2))),
id     └───┘           └┘              
src    └───┘               └┘                  
typ    └───┘                         
doc    └───┘
692    from funext $ assume f, map_eq_comap_of_inverse
id          └────┘            └─────────────────────┘
src         └────┘             └─────────────────────┘
typ         └────┘            └─────────────────────┘
693      (funext $ assume ⟨⟨_, _⟩, ⟨_, _⟩⟩, rfl) (funext $ assume ⟨⟨_, _⟩, ⟨_, _⟩⟩, rfl),
id        └────┘                           └─┘   └────┘                           └─┘
src       └────┘                            └─┘   └────┘                            └─┘
typ       └────┘                           └─┘   └────┘                           └─┘
694  by rw [this, uniformity_prod, filter.prod, comap_inf, comap_comap_comp, comap_comap_comp]
id          └──┘  └─────────────┘  └─────────┘  └───────┘  └──────────────┘  └──────────────┘
src     └──┘    └┘└─────────────┘└┘└─────────┘└┘└───────┘└┘└──────────────┘└┘└──────────────┘└─
typ     └──┘└──┘└┘└─────────────┘└┘└─────────┘└┘└───────┘└┘└──────────────┘└┘└──────────────┘└─
doc     └──┘    └┘               └┘└─────────┘└┘         └┘                └┘                └─
txt     └──┘    └┘               └┘           └┘         └┘                └┘                └─
par     └──┘    └┘               └┘           └┘         └┘                └┘                └─
pid       └┘    └┘               └┘           └┘         └┘                └┘                
st     └───────┘└───────────────┘└───────────┘└─────────┘└────────────────┘└────────────────┘
695  
src  
typ  
doc  
txt  
par  
pid  
st   
696  lemma mem_map_sets_iff' {α : Type*} {β : Type*} {f : filter α} {m : α → β} {t : set β} :
id                                                        └────┘                  └─┘ 
src                                                       └────┘                     └─┘
typ                                                       └────┘                  └─┘ 
697    t ∈ (map m f).sets ↔ (∃s∈f, m '' s ⊆ t) :=
id        └─┘   └──┘       └┘   
src        └─┘     └──┘          └┘   
typ       └─┘   └──┘       └┘   
doc         └─┘
698  mem_map_sets_iff
id   └──────────────┘
src  └──────────────┘
typ  └──────────────┘
699  
700  lemma mem_uniformity_of_uniform_continuous_invariant [uniform_space α] {s:set (α×α)} {f : α → α → α}
id                                                         └───────────┘      └─┘                
src                                                        └───────────┘       └─┘   
typ                                                        └───────────┘      └─┘                
doc                                                        └───────────┘
701    (hf : uniform_continuous (λp:α×α, f p.1 p.2)) (hs : s ∈ 𝓤 α) :
id           └────────────────┘                       
src          └────────────────┘                            
typ          └────────────────┘                       
doc                                                            
702    ∃u∈𝓤 α, ∀a b c, (a, b) ∈ u → (f a c, f b c) ∈ s :=
id                              
src                                          
typ                             
doc       
703  begin
st   └─────
704    rw [uniform_continuous, uniformity_prod_eq_prod, tendsto_map'_iff, (∘)] at hf,
id         └────────────────┘  └─────────────────────┘  └──────────────┘  
src    └──┘└────────────────┘└┘└─────────────────────┘└┘└──────────────┘└┘└───────┘
typ    └──┘└────────────────┘└┘└─────────────────────┘└┘└──────────────┘└┘└───────┘
doc    └──┘                  └┘                       └┘                └┘ └───────┘
txt    └──┘                  └┘                       └┘                └┘ └───────┘
par    └──┘                  └┘                       └┘                └┘ └───────┘
pid      └┘                  └┘                       └┘                └┘ └─┘└────┘
st   ───────────────────────┘└───────────────────────┘└────────────────┘└───┘└────┘└─
705    rcases mem_map_sets_iff'.1 (hf hs) with ⟨t, ht, hts⟩, clear hf,
id            └───────────────┘    └┘ └┘
src    └─────┘└───────────────┘└─┘     └─────────────────┘  └──────┘
typ    └─────┘└───────────────┘└─┘ └┘└┘└─────────────────┘  └──────┘
doc    └─────┘                 └─┘     └─────────────────┘  └──────┘
txt    └─────┘                 └─┘     └─────────────────┘  └──────┘
par    └─────┘                 └─┘     └─────────────────┘  └──────┘
pid                           └─┘     └─────────────────┘       └─┘
st   ─────────────────────────────────────────────────────┘└────────┘└─
706    rcases mem_prod_iff.1 ht with ⟨u, hu, v, hv, huvt⟩, clear ht,
id            └──────────┘   └┘
src    └─────┘└──────────┘└─┘  └────────────────────────┘  └──────┘
typ    └─────┘└──────────┘└─┘└┘└────────────────────────┘  └──────┘
doc    └─────┘            └─┘  └────────────────────────┘  └──────┘
txt    └─────┘            └─┘  └────────────────────────┘  └──────┘
par    └─────┘            └─┘  └────────────────────────┘  └──────┘
pid                      └─┘  └────────────────────────┘       └─┘
st   ───────────────────────────────────────────────────┘└────────┘└─
707    refine ⟨u, hu, assume a b c hab, hts $ (mem_image _ _ _).2 ⟨⟨⟨a, b⟩, ⟨c, c⟩⟩, huvt ⟨_, _⟩, _⟩⟩,
id               └┘                    └─┘    └───────┘                             └──┘
src    └─────┘  └┘  └┘      └──────────┘     └───────┘└────────┘    └┘ └─┘  └┘ └──┘     └────────┘
typ    └─────┘ └┘└┘└┘      └──────────┘└─┘  └───────┘└────────┘    └┘ └─┘  └┘ └──┘└──┘ └────────┘
doc    └─────┘  └┘  └┘      └──────────┘              └────────┘    └┘ └─┘  └┘ └──┘     └────────┘
txt    └─────┘  └┘  └┘      └──────────┘              └────────┘    └┘ └─┘  └┘ └──┘     └────────┘
par    └─────┘  └┘  └┘      └──────────┘              └────────┘    └┘ └─┘  └┘ └──┘     └────────┘
pid            └┘  └┘      └──────────┘              └────────┘    └┘ └─┘  └┘ └──┘     └────────┘
st   ───────────────────────────────────────────────────────────────────────────────────────────────┘└─
708    exact hab,
id           └─┘
src    └────┘
typ    └────┘└─┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ──────────┘└─
709    exact refl_mem_uniformity hv,
id           └─────────────────┘ └┘
src    └────┘└─────────────────┘
typ    └────┘└─────────────────┘└┘
doc    └────┘                   
txt    └────┘                   
par    └────┘                   
pid                            
st   ─────────────────────────────┘└─
710    refl
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid        
st   ──────┘
711  end
st   └─┘
712  
713  lemma mem_uniform_prod [t₁ : uniform_space α] [t₂ : uniform_space β] {a : set (α × α)} {b : set (β × β)}
id                                └───────────┘         └───────────┘        └─┘            └─┘    
src                               └───────────┘          └───────────┘         └─┘              └─┘    
typ                               └───────────┘         └───────────┘        └─┘            └─┘    
doc                               └───────────┘          └───────────┘
714    (ha : a ∈ 𝓤 α) (hb : b ∈ 𝓤 β) :
id                         
src                          
typ                        
doc                            
715    {p:(α×β)×(α×β) | (p.1.1, p.2.1) ∈ a ∧ (p.1.2, p.2.2) ∈ b } ∈ (@uniformity (α × β) _) :=
id                                        └────────┘    
src                                                 └────────┘    
typ                                       └────────┘    
doc                                                                   └────────┘
716  by rw [uniformity_prod]; exact inter_mem_inf_sets (preimage_mem_comap ha) (preimage_mem_comap hb)
id          └─────────────┘         └────────────────┘                     └┘   └────────────────┘ └┘
src     └──┘└─────────────┘  └────┘└────────────────┘                     └┘ └────────────────┘  └─
typ     └──┘└─────────────┘  └────┘└────────────────┘                   └┘└┘ └────────────────┘└┘└─
doc     └──┘                 └────┘                                       └┘                     └─
txt     └──┘                 └────┘                                       └┘                     └─
par     └──┘                 └────┘                                       └┘                     └─
pid       └┘                                                             └┘                     
st     └──────────────────┘└──────────────────────────────────────────────────────────────────────────
717  
src  
typ  
doc  
txt  
par  
pid  
st   
718  lemma tendsto_prod_uniformity_fst [uniform_space α] [uniform_space β] :
id                                      └───────────┘    └───────────┘ 
src                                     └───────────┘     └───────────┘
typ                                     └───────────┘    └───────────┘ 
doc                                     └───────────┘     └───────────┘
719    tendsto (λp:(α×β)×(α×β), (p.1.1, p.2.1)) (𝓤 (α × β)) (𝓤 α) :=
id     └─────┘                              
src    └─────┘                                     
typ    └─────┘                              
doc    └─────┘                                              
720  le_trans (map_mono (@inf_le_left (uniform_space (α×β)) _ _ _)) map_comap_le
id   └──────┘  └──────┘   └─────────┘  └───────────┘             └──────────┘
src  └──────┘  └──────┘   └─────────┘  └───────────┘               └──────────┘
typ  └──────┘  └──────┘   └─────────┘  └───────────┘             └──────────┘
doc                                    └───────────┘
721  
722  lemma tendsto_prod_uniformity_snd [uniform_space α] [uniform_space β] :
id                                      └───────────┘    └───────────┘ 
src                                     └───────────┘     └───────────┘
typ                                     └───────────┘    └───────────┘ 
doc                                     └───────────┘     └───────────┘
723    tendsto (λp:(α×β)×(α×β), (p.1.2, p.2.2)) (𝓤 (α × β)) (𝓤 β) :=
id     └─────┘                              
src    └─────┘                                     
typ    └─────┘                              
doc    └─────┘                                              
724  le_trans (map_mono (@inf_le_right (uniform_space (α×β)) _ _ _)) map_comap_le
id   └──────┘  └──────┘   └──────────┘  └───────────┘             └──────────┘
src  └──────┘  └──────┘   └──────────┘  └───────────┘               └──────────┘
typ  └──────┘  └──────┘   └──────────┘  └───────────┘             └──────────┘
doc                                     └───────────┘
725  
726  lemma uniform_continuous_fst [uniform_space α] [uniform_space β] : uniform_continuous (λp:α×β, p.1) :=
id                                 └───────────┘    └───────────┘     └────────────────┘       
src                                └───────────┘     └───────────┘      └────────────────┘          
typ                                └───────────┘    └───────────┘     └────────────────┘       
doc                                └───────────┘     └───────────┘
727  tendsto_prod_uniformity_fst
id   └─────────────────────────┘
src  └─────────────────────────┘
typ  └─────────────────────────┘
728  
729  lemma uniform_continuous_snd [uniform_space α] [uniform_space β] : uniform_continuous (λp:α×β, p.2) :=
id                                 └───────────┘    └───────────┘     └────────────────┘       
src                                └───────────┘     └───────────┘      └────────────────┘          
typ                                └───────────┘    └───────────┘     └────────────────┘       
doc                                └───────────┘     └───────────┘
730  tendsto_prod_uniformity_snd
id   └─────────────────────────┘
src  └─────────────────────────┘
typ  └─────────────────────────┘
731  
732  variables [uniform_space α] [uniform_space β] [uniform_space γ]
id              └───────────┘     └───────────┘     └───────────┘
src             └───────────┘     └───────────┘     └───────────┘
typ             └───────────┘     └───────────┘     └───────────┘
doc             └───────────┘     └───────────┘     └───────────┘
733  lemma uniform_continuous.prod_mk
734    {f₁ : α → β} {f₂ : α → γ} (h₁ : uniform_continuous f₁) (h₂ : uniform_continuous f₂) :
id                                 └────────────────┘ └┘        └────────────────┘ └┘
src                                    └────────────────┘           └────────────────┘
typ                                └────────────────┘ └┘        └────────────────┘ └┘
735    uniform_continuous (λa, (f₁ a, f₂ a)) :=
id     └────────────────┘     └┘   └┘ 
src    └────────────────┘      
typ    └────────────────┘     └┘   └┘ 
736  by rw [uniform_continuous, uniformity_prod]; exact
id          └────────────────┘  └─────────────┘
src     └──┘└────────────────┘└┘└─────────────┘  └────┘
typ     └──┘└────────────────┘└┘└─────────────┘  └────┘
doc     └──┘                  └┘                 └────┘
txt     └──┘                  └┘                 └────┘
par     └──┘                  └┘                 └────┘
pid       └┘                  └┘                      
st     └─────────────────────┘└───────────────┘└───────
737  tendsto_inf.2 ⟨tendsto_comap_iff.2 h₁, tendsto_comap_iff.2 h₂⟩
id   └─────────┘                        └┘  └───────────────┘   └┘
src  └─────────┘└─┘                  └─┘  └┘└───────────────┘└─┘  └─
typ  └─────────┘└─┘                  └─┘└┘└┘└───────────────┘└─┘└┘└─
doc             └─┘                  └─┘  └┘                 └─┘  └─
txt             └─┘                  └─┘  └┘                 └─┘  └─
par             └─┘                  └─┘  └┘                 └─┘  └─
pid             └─┘                  └─┘  └┘                 └─┘  
st   ───────────────────────────────────────────────────────────────
738  
src  
typ  
doc  
txt  
par  
pid  
st   
739  lemma uniform_continuous.prod_mk_left {f : α × β → γ} (h : uniform_continuous f) (b) :
id                                                          └────────────────┘ 
src                                                            └────────────────┘
typ                                                         └────────────────┘ 
740    uniform_continuous (λ a, f (a,b)) :=
id     └────────────────┘        
src    └────────────────┘         
typ    └────────────────┘        
741  h.comp (uniform_continuous_id.prod_mk uniform_continuous_const)
id   └───┘  └───────────────────┘└──────┘ └──────────────────────┘
src   └───┘  └───────────────────┘└──────┘ └──────────────────────┘
typ  └───┘  └───────────────────┘└──────┘ └──────────────────────┘
742  
743  lemma uniform_continuous.prod_mk_right {f : α × β → γ} (h : uniform_continuous f) (a) :
id                                                           └────────────────┘ 
src                                                             └────────────────┘
typ                                                          └────────────────┘ 
744    uniform_continuous (λ b, f (a,b)) :=
id     └────────────────┘        
src    └────────────────┘         
typ    └────────────────┘        
745  h.comp (uniform_continuous_const.prod_mk  uniform_continuous_id)
id   └───┘  └──────────────────────┘└──────┘  └───────────────────┘
src   └───┘  └──────────────────────┘└──────┘  └───────────────────┘
typ  └───┘  └──────────────────────┘└──────┘  └───────────────────┘
746  
747  lemma to_topological_space_prod {α} {β} [u : uniform_space α] [v : uniform_space β] :
id                                                └───────────┘        └───────────┘ 
src                                               └───────────┘         └───────────┘
typ                                               └───────────┘        └───────────┘ 
doc                                               └───────────┘         └───────────┘
748    @uniform_space.to_topological_space (α × β) prod.uniform_space =
id      └────────────────────────────────┘      └────────────────┘ 
src     └────────────────────────────────┘        └────────────────┘ 
typ     └────────────────────────────────┘      └────────────────┘ 
749      @prod.topological_space α β u.to_topological_space v.to_topological_space := rfl
id        └────────────────────┘   └───────────────────┘ └───────────────────┘    └─┘
src       └────────────────────┘      └───────────────────┘  └───────────────────┘    └─┘
typ       └────────────────────┘   └───────────────────┘ └───────────────────┘    └─┘
750  
751  end prod
752  
753  section
754  open uniform_space function
755  variables [uniform_space α] [uniform_space β] [uniform_space γ] [uniform_space δ]
id              └───────────┘     └───────────┘     └───────────┘     └───────────┘
src             └───────────┘     └───────────┘     └───────────┘     └───────────┘
typ             └───────────┘     └───────────┘     └───────────┘     └───────────┘
doc             └───────────┘     └───────────┘     └───────────┘     └───────────┘
756  
757  local notation f `∘₂` g := function.bicompr f g
id                              └──────────────┘
src                             └──────────────┘
typ                             └──────────────┘
758  
759  def uniform_continuous₂ (f : α → β → γ) := uniform_continuous (uncurry' f)
id                                           └────────────────┘  └──────┘ 
src                                             └────────────────┘  └──────┘
typ                                          └────────────────┘  └──────┘ 
760  
761  lemma uniform_continuous₂_def (f : α → β → γ) : uniform_continuous₂ f ↔ uniform_continuous (uncurry' f) := iff.rfl
id                                                └─────────────────┘   └────────────────┘  └──────┘      └─────┘
src                                                  └─────────────────┘    └────────────────┘  └──────┘       └─────┘
typ                                               └─────────────────┘   └────────────────┘  └──────┘      └─────┘
762  
763  lemma uniform_continuous₂_curry (f : α × β → γ) : uniform_continuous₂ (function.curry f) ↔ uniform_continuous f :=
id                                                 └─────────────────┘  └────────────┘    └────────────────┘ 
src                                                   └─────────────────┘  └────────────┘     └────────────────┘
typ                                                └─────────────────┘  └────────────┘    └────────────────┘ 
764  by rw  [←uncurry'_curry f] {occs := occurrences.pos [2]} ; refl
id            └────────────┘            └─────────────┘  
src     └────┘└────────────┘ └┘ └──────┘└─────────────┘└┘  └────
typ     └────┘└────────────┘└┘ └──────┘└─────────────┘└┘  └────
doc     └────┘               └┘ └──────┘                 └┘  └────
txt     └────┘               └┘ └──────┘                 └┘  └────
par     └────┘               └┘ └──────┘                 └┘  └────
pid       └──┘                └──────┘                       
st     └─────────────────────┘└─────────────────────────────────────
765  
src  
typ  
doc  
txt  
par  
pid  
st   
766  lemma uniform_continuous₂.comp {f : α → β → γ} {g : γ → δ}
id                                                       
typ                                                      
767    (hg : uniform_continuous g) (hf : uniform_continuous₂ f) :
id           └────────────────┘         └─────────────────┘ 
src          └────────────────┘          └─────────────────┘
typ          └────────────────┘         └─────────────────┘ 
768    uniform_continuous₂ (g ∘₂ f) :=
id     └─────────────────┘   └┘ 
src    └─────────────────┘    └┘
typ    └─────────────────┘   └┘ 
769  hg.comp hf
id   └┘└───┘ └┘
src    └───┘
typ  └┘└───┘ └┘
770  
771  end
772  
773  lemma to_topological_space_subtype [u : uniform_space α] {p : α → Prop} :
id                                           └───────────┘        
src                                          └───────────┘
typ                                          └───────────┘        
doc                                          └───────────┘
774    @uniform_space.to_topological_space (subtype p) subtype.uniform_space =
id      └────────────────────────────────┘  └─────┘   └───────────────────┘ 
src     └────────────────────────────────┘  └─────┘    └───────────────────┘ 
typ     └────────────────────────────────┘  └─────┘   └───────────────────┘ 
775      @subtype.topological_space α p u.to_topological_space := rfl
id        └───────────────────────┘   └───────────────────┘    └─┘
src       └───────────────────────┘      └───────────────────┘    └─┘
typ       └───────────────────────┘   └───────────────────┘    └─┘
776  
777  section sum
778  variables [uniform_space α] [uniform_space β]
id              └───────────┘     └───────────┘
src             └───────────┘     └───────────┘
typ             └───────────┘     └───────────┘
doc             └───────────┘     └───────────┘
779  open sum
780  
781  /-- Uniformity on a disjoint union. Entourages of the diagonal in the union are obtained
782  by taking independently an entourage of the diagonal in the first part, and an entourage of
783  the diagonal in the second part. -/
784  def uniform_space.core.sum : uniform_space.core (α ⊕ β) :=
id                                └────────────────┘    
src                               └────────────────┘    
typ                               └────────────────┘    
doc                               └────────────────┘
785  uniform_space.core.mk'
id   └────────────────────┘
src  └────────────────────┘
typ  └────────────────────┘
786    (map (λ p : α × α, (inl p.1, inl p.2)) (𝓤 α) ⊔ map (λ p : β × β, (inr p.1, inr p.2)) (𝓤 β))
id      └─┘            └─┘    └─┘          └─┘            └─┘    └─┘       
src     └─┘              └─┘     └─┘            └─┘              └─┘     └─┘       
typ     └─┘            └─┘    └─┘          └─┘            └─┘    └─┘       
doc     └─┘                                          └─┘                                    
787    (λ r ⟨H₁, H₂⟩ x, by cases x; [apply refl_mem_uniformity H₁, apply refl_mem_uniformity H₂])
id                                    └─────────────────┘ └┘        └─────────────────┘ └┘
src                        └────┘   └────┘└─────────────────┘    └────┘└─────────────────┘
typ                     └────┘  └────┘└─────────────────┘└┘  └────┘└─────────────────┘└┘
doc                        └────┘    └────┘                       └────┘                   
txt                        └────┘    └────┘                       └────┘                   
par                        └────┘    └────┘                       └────┘                   
pid                                                                                     
st                        └────────────────────────────────────────────────────────────────────┘
788    (λ r ⟨H₁, H₂⟩, ⟨symm_le_uniformity H₁, symm_le_uniformity H₂⟩)
id         └┘  └┘    └────────────────┘     └────────────────┘
src                    └────────────────┘     └────────────────┘
typ        └┘  └┘    └────────────────┘     └────────────────┘
789    (λ r ⟨Hrα, Hrβ⟩, begin
id         
typ        
st                      └─────
790      rcases comp_mem_uniformity_sets Hrα with ⟨tα, htα, Htα⟩,
id              └──────────────────────┘ └─┘
src      └─────┘└──────────────────────┘   └──────────────────┘
typ      └─────┘└──────────────────────┘└─┘└──────────────────┘
doc      └─────┘                           └──────────────────┘
txt      └─────┘                           └──────────────────┘
par      └─────┘                           └──────────────────┘
pid                                       └──────────────────┘
st   ──────────────────────────────────────────────────────────┘└─
791      rcases comp_mem_uniformity_sets Hrβ with ⟨tβ, htβ, Htβ⟩,
id              └──────────────────────┘ └─┘
src      └─────┘└──────────────────────┘   └──────────────────┘
typ      └─────┘└──────────────────────┘└─┘└──────────────────┘
doc      └─────┘                           └──────────────────┘
txt      └─────┘                           └──────────────────┘
par      └─────┘                           └──────────────────┘
pid                                       └──────────────────┘
st   ──────────────────────────────────────────────────────────┘└─
792      refine ⟨_,
src      └─────┘ └──
typ      └─────┘ └──
doc      └─────┘ └──
txt      └─────┘ └──
par      └─────┘ └──
pid             └──
st   ───────────────
793        ⟨mem_map_sets_iff.2 ⟨tα, htα, subset_union_left _ _⟩,
id                              └┘  └─┘  └───────────────┘
src  ─────┘                 └─┘   └┘   └┘└───────────────┘└──────
typ  ─────┘                 └─┘ └┘└┘└─┘└┘└───────────────┘└──────
doc  ─────┘                 └─┘   └┘   └┘                 └──────
txt  ─────┘                 └─┘   └┘   └┘                 └──────
par  ─────┘                 └─┘   └┘   └┘                 └──────
pid  ─────┘                 └─┘   └┘   └┘                 └──────
st   ────────────────────────────────────────────────────────────
794         mem_map_sets_iff.2 ⟨tβ, htβ, subset_union_right _ _⟩⟩, _⟩,
id          └──────────────┘    └┘  └─┘  └────────────────┘
src  ──────┘└──────────────┘└─┘   └┘   └┘└────────────────┘└────────┘
typ  ──────┘└──────────────┘└─┘ └┘└┘└─┘└┘└────────────────┘└────────┘
doc  ──────┘                └─┘   └┘   └┘                  └────────┘
txt  ──────┘                └─┘   └┘   └┘                  └────────┘
par  ──────┘                └─┘   └┘   └┘                  └────────┘
pid  ──────┘                └─┘   └┘   └┘                  └────────┘
st   ───────────────────────────────────────────────────────────────┘└─
795      rintros ⟨_, _⟩ ⟨z, ⟨⟨a, b⟩, hab, ⟨⟩⟩ | ⟨⟨a, b⟩, hab, ⟨⟩⟩,
src      └─────────────────────────────────────────────────────────
typ      └─────────────────────────────────────────────────────────
doc      └─────────────────────────────────────────────────────────
txt      └─────────────────────────────────────────────────────────
par      └─────────────────────────────────────────────────────────
pid             └──────────────────────────────────────────────────
st   ──────────────────────────────────────────────────────────────
796                         ⟨⟨_, c⟩, hbc, ⟨⟩⟩ | ⟨⟨_, c⟩, hbc, ⟨⟩⟩⟩,
src  ────────────────────────────────────────────────────────────┘
typ  ────────────────────────────────────────────────────────────┘
doc  ────────────────────────────────────────────────────────────┘
txt  ────────────────────────────────────────────────────────────┘
par  ────────────────────────────────────────────────────────────┘
pid  ────────────────────────────────────────────────────────────┘
st   ────────────────────────────────────────────────────────────┘└─
797      { have A : (a, c) ∈ comp_rel tα tα := ⟨b, hab, hbc⟩,
id                       └──────┘    └┘       └─┘  └─┘
src        └───────┘ └┘ └┘└──────┘    └──┘  └┘   └┘   
typ        └───────┘└┘└┘└──────┘  └┘└──┘ └┘└─┘└┘└─┘
doc        └───────┘  └┘ └┘ └──────┘    └──┘  └┘   └┘   
txt        └───────┘  └┘ └┘             └──┘  └┘   └┘   
par        └───────┘  └┘ └┘             └──┘  └┘   └┘   
pid        └────┘└─┘  └┘ └┘             └──┘  └┘   └┘   
st   ─────┘└───────────────────────────────────────────────┘└─
798        exact Htα A },
id               └─┘ 
src        └────┘    
typ        └────┘└─┘
doc        └────┘    
txt        └────┘    
par        └────┘    
pid                 
st   ─────────────────┘└┘
799      { have A : (a, c) ∈ comp_rel tβ tβ := ⟨b, hab, hbc⟩,
id                        └──────┘    └┘       └─┘  └─┘
src        └───────┘ └┘ └┘ └──────┘    └──┘  └┘   └┘   
typ        └───────┘└┘└┘ └──────┘  └┘└──┘ └┘└─┘└┘└─┘
doc        └───────┘  └┘ └┘ └──────┘    └──┘  └┘   └┘   
txt        └───────┘  └┘ └┘             └──┘  └┘   └┘   
par        └───────┘  └┘ └┘             └──┘  └┘   └┘   
pid        └────┘└─┘  └┘ └┘             └──┘  └┘   └┘   
st   ──────────────────────────────────────────────────────┘└─
800        exact Htβ A }
id               └─┘ 
src        └────┘    
typ        └────┘└─┘
doc        └────┘    
txt        └────┘    
par        └────┘    
pid                 
st   ─────────────────┘└─
801    end)
st   ────┘
802  
803  /-- The union of an entourage of the diagonal in each set of a disjoint union is again an entourage of the diagonal. -/
804  lemma union_mem_uniformity_sum
805    {a : set (α × α)} (ha : a ∈ 𝓤 α) {b : set (β × β)} (hb : b ∈ 𝓤 β) :
id          └─┘                       └─┘                
src         └─┘                           └─┘                  
typ         └─┘                       └─┘                
doc                                                                
806    ((λ p : (α × α), (inl p.1, inl p.2)) '' a ∪ (λ p : (β × β), (inr p.1, inr p.2)) '' b) ∈ (@uniform_space.core.sum α β _ _).uniformity :=
id                   └─┘    └─┘     └┘                └─┘    └─┘     └┘      └────────────────────┘       └────────┘
src                    └─┘     └─┘      └┘                   └─┘     └─┘      └┘       └────────────────────┘         └────────┘
typ                  └─┘    └─┘     └┘                └─┘    └─┘     └┘      └────────────────────┘       └────────┘
doc                                                                                              └────────────────────┘
807  ⟨mem_map_sets_iff.2 ⟨_, ha, subset_union_left _ _⟩, mem_map_sets_iff.2 ⟨_, hb, subset_union_right _ _⟩⟩
id    └──────────────┘      └┘  └───────────────┘       └──────────────┘      └┘  └────────────────┘
src   └──────────────┘          └───────────────┘       └──────────────┘          └────────────────┘
typ   └──────────────┘      └┘  └───────────────┘       └──────────────┘      └┘  └────────────────┘
808  
809  /- To prove that the topology defined by the uniform structure on the disjoint union coincides with
810  the disjoint union topology, we need two lemmas saying that open sets can be characterized by
811  the uniform structure -/
812  lemma uniformity_sum_of_open_aux {s : set (α ⊕ β)} (hs : is_open s) {x : α ⊕ β} (xs : x ∈ s) :
id                                         └─┘             └─────┘                    
src                                        └─┘               └─────┘                       
typ                                        └─┘             └─────┘                    
doc                                                           └─────┘
813    { p : ((α ⊕ β) × (α ⊕ β)) | p.1 = x → p.2 ∈ s } ∈ (@uniform_space.core.sum α β _ _).uniformity :=
id                                        └────────────────────┘       └────────┘
src                                               └────────────────────┘         └────────┘
typ                                       └────────────────────┘       └────────┘
doc                                                        └────────────────────┘
814  begin
st   └─────
815    cases x,
id           
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ────────┘└─
816    { refine mem_sets_of_superset
id              └──────────────────┘
src      └─────┘└──────────────────┘
typ      └─────┘└──────────────────┘
doc      └─────┘                    
txt      └─────┘                    
par      └─────┘                    
pid                                
st   ───┘└───────────────────────────
817        (union_mem_uniformity_sum (mem_nhds_uniformity_iff.1 (mem_nhds_sets hs.1 xs)) univ_mem_sets)
id          └──────────────────────┘  └─────────────────────┘    └───────────┘ └┘   └┘   └───────────┘
src  ─────┘ └──────────────────────┘ └─────────────────────┘└─┘ └───────────┘  └─┘  └─┘└───────────┘└─
typ  ─────┘ └──────────────────────┘ └─────────────────────┘└─┘ └───────────┘└┘└─┘└┘└─┘└───────────┘└─
doc  ─────┘ └──────────────────────┘                        └─┘                └─┘  └─┘             └─
txt  ─────┘                                                 └─┘                └─┘  └─┘             └─
par  ─────┘                                                 └─┘                └─┘  └─┘             └─
pid  ─────┘                                                 └─┘                └─┘  └─┘             └─
st   ───────────────────────────────────────────────────────────────────────────────────────────────────
818        (union_subset _ _);
id          └──────────┘
src  ─────┘ └──────────┘└───┘
typ  ─────┘ └──────────┘└───┘
doc  ─────┘             └───┘
txt  ─────┘             └───┘
par  ─────┘             └───┘
pid  ─────┘             └───┘
st   ──────────────────────────
819      rintro _ ⟨⟨_, b⟩, h, ⟨⟩⟩ ⟨⟩,
src      └─────────────────────────┘
typ      └─────────────────────────┘
doc      └─────────────────────────┘
txt      └─────────────────────────┘
par      └─────────────────────────┘
pid            └───────────────────┘
st   ──────────────────────────────┘└─
820      exact h rfl },
id              └─┘
src      └────┘ └─┘
typ      └────┘└─┘
doc      └────┘    
txt      └────┘    
par      └────┘    
pid               
st   ───────────────┘└┘
821    { refine mem_sets_of_superset
id              └──────────────────┘
src      └─────┘└──────────────────┘
typ      └─────┘└──────────────────┘
doc      └─────┘                    
txt      └─────┘                    
par      └─────┘                    
pid                                
st   ────────────────────────────────
822        (union_mem_uniformity_sum univ_mem_sets (mem_nhds_uniformity_iff.1 (mem_nhds_sets hs.2 xs)))
id          └──────────────────────┘ └───────────┘  └─────────────────────┘    └───────────┘ └┘   └┘
src  ─────┘ └──────────────────────┘└───────────┘ └─────────────────────┘└─┘ └───────────┘  └─┘  └───
typ  ─────┘ └──────────────────────┘└───────────┘ └─────────────────────┘└─┘ └───────────┘└┘└─┘└┘└───
doc  ─────┘ └──────────────────────┘                                     └─┘                └─┘  └───
txt  ─────┘                                                              └─┘                └─┘  └───
par  ─────┘                                                              └─┘                └─┘  └───
pid  ─────┘                                                              └─┘                └─┘  └───
st   ───────────────────────────────────────────────────────────────────────────────────────────────────
823        (union_subset _ _);
id          └──────────┘
src  ─────┘ └──────────┘└───┘
typ  ─────┘ └──────────┘└───┘
doc  ─────┘             └───┘
txt  ─────┘             └───┘
par  ─────┘             └───┘
pid  ─────┘             └───┘
st   ──────────────────────────
824      rintro _ ⟨⟨a, _⟩, h, ⟨⟩⟩ ⟨⟩,
src      └─────────────────────────┘
typ      └─────────────────────────┘
doc      └─────────────────────────┘
txt      └─────────────────────────┘
par      └─────────────────────────┘
pid            └───────────────────┘
st   ──────────────────────────────┘└─
825      exact h rfl },
id              └─┘
src      └────┘ └─┘
typ      └────┘└─┘
doc      └────┘    
txt      └────┘    
par      └────┘    
pid               
st   ───────────────┘└──
826  end
st   ──┘
827  
828  lemma open_of_uniformity_sum_aux {s : set (α ⊕ β)}
id                                         └─┘    
src                                        └─┘    
typ                                        └─┘    
829    (hs : ∀x ∈ s, { p : ((α ⊕ β) × (α ⊕ β)) | p.1 = x → p.2 ∈ s } ∈ (@uniform_space.core.sum α β _ _).uniformity) :
id                                                    └────────────────────┘       └────────┘
src                                                             └────────────────────┘         └────────┘
typ                                                   └────────────────────┘       └────────┘
doc                                                                      └────────────────────┘
830    is_open s :=
id     └─────┘ 
src    └─────┘
typ    └─────┘ 
doc    └─────┘
831  begin
st   └─────
832    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
833    { refine (@is_open_iff_mem_nhds α _ _).2 (λ a ha, mem_nhds_uniformity_iff.2 _),
id                └──────────────────┘                  └─────────────────────┘
src      └─────┘  └──────────────────┘ └──────┘  └─────┘└─────────────────────┘└───┘
typ      └─────┘  └──────────────────┘└──────┘  └─────┘└─────────────────────┘└───┘
doc      └─────┘                       └──────┘  └─────┘                       └───┘
txt      └─────┘                       └──────┘  └─────┘                       └───┘
par      └─────┘                       └──────┘  └─────┘                       └───┘
pid                                   └──────┘  └─────┘                       └───┘
st   ───┘└──────────────────────────────────────────────────────────────────────────┘└─
834      rcases mem_map_sets_iff.1 (hs _ ha).1 with ⟨t, ht, st⟩,
id              └──────────────┘    └┘   └┘
src      └─────┘└──────────────┘└─┘   └─┘  └──────────────────┘
typ      └─────┘└──────────────┘└─┘ └┘└─┘└┘└──────────────────┘
doc      └─────┘                └─┘   └─┘  └──────────────────┘
txt      └─────┘                └─┘   └─┘  └──────────────────┘
par      └─────┘                └─┘   └─┘  └──────────────────┘
pid                            └─┘   └─┘  └──────────────────┘
st   ─────────────────────────────────────────────────────────┘└─
835      refine mem_sets_of_superset ht _,
id              └──────────────────┘ └┘
src      └─────┘└──────────────────┘  └┘
typ      └─────┘└──────────────────┘└┘└┘
doc      └─────┘                      └┘
txt      └─────┘                      └┘
par      └─────┘                      └┘
pid                                  └┘
st   ───────────────────────────────────┘└─
836      rintro p pt rfl, exact st ⟨_, pt, rfl⟩ rfl },
id                              └┘     └┘       └─┘
src      └─────────────┘  └────┘   └─┘  └┘   └┘└─┘
typ      └─────────────┘  └────┘└┘ └─┘└┘└┘   └┘└─┘
doc      └─────────────┘  └────┘   └─┘  └┘   └┘   
txt      └─────────────┘  └────┘   └─┘  └┘   └┘   
par      └─────────────┘  └────┘   └─┘  └┘   └┘   
pid            └───────┘          └─┘  └┘   └┘   
st   ──────────────────┘└──────────────────────────┘└┘
837    { refine (@is_open_iff_mem_nhds β _ _).2 (λ b hb, mem_nhds_uniformity_iff.2 _),
id                └──────────────────┘                  └─────────────────────┘
src      └─────┘  └──────────────────┘ └──────┘  └─────┘└─────────────────────┘└───┘
typ      └─────┘  └──────────────────┘└──────┘  └─────┘└─────────────────────┘└───┘
doc      └─────┘                       └──────┘  └─────┘                       └───┘
txt      └─────┘                       └──────┘  └─────┘                       └───┘
par      └─────┘                       └──────┘  └─────┘                       └───┘
pid                                   └──────┘  └─────┘                       └───┘
st   ───────────────────────────────────────────────────────────────────────────────┘└─
838      rcases mem_map_sets_iff.1 (hs _ hb).2 with ⟨t, ht, st⟩,
id              └──────────────┘    └┘   └┘
src      └─────┘└──────────────┘└─┘   └─┘  └──────────────────┘
typ      └─────┘└──────────────┘└─┘ └┘└─┘└┘└──────────────────┘
doc      └─────┘                └─┘   └─┘  └──────────────────┘
txt      └─────┘                └─┘   └─┘  └──────────────────┘
par      └─────┘                └─┘   └─┘  └──────────────────┘
pid                            └─┘   └─┘  └──────────────────┘
st   ─────────────────────────────────────────────────────────┘└─
839      refine mem_sets_of_superset ht _,
id              └──────────────────┘ └┘
src      └─────┘└──────────────────┘  └┘
typ      └─────┘└──────────────────┘└┘└┘
doc      └─────┘                      └┘
txt      └─────┘                      └┘
par      └─────┘                      └┘
pid                                  └┘
st   ───────────────────────────────────┘└─
840      rintro p pt rfl, exact st ⟨_, pt, rfl⟩ rfl }
id                              └┘     └┘       └─┘
src      └─────────────┘  └────┘   └─┘  └┘   └┘└─┘
typ      └─────────────┘  └────┘└┘ └─┘└┘└┘   └┘└─┘
doc      └─────────────┘  └────┘   └─┘  └┘   └┘   
txt      └─────────────┘  └────┘   └─┘  └┘   └┘   
par      └─────────────┘  └────┘   └─┘  └┘   └┘   
pid            └───────┘          └─┘  └┘   └┘   
st   ──────────────────┘└──────────────────────────┘└─
841  end
st   ──┘
842  
843  /- We can now define the uniform structure on the disjoint union -/
844  instance sum.uniform_space : uniform_space (α ⊕ β) :=
id                                └───────────┘    
src                               └───────────┘    
typ                               └───────────┘    
doc                               └───────────┘
845  { to_core := uniform_space.core.sum,
id                └────────────────────┘
src               └────────────────────┘
typ               └────────────────────┘
doc               └────────────────────┘
846    is_open_uniformity := λ s, ⟨uniformity_sum_of_open_aux, open_of_uniformity_sum_aux⟩ }
id                                └────────────────────────┘  └────────────────────────┘
src                                └────────────────────────┘  └────────────────────────┘
typ                               └────────────────────────┘  └────────────────────────┘
847  
848  lemma sum.uniformity : 𝓤 (α ⊕ β) =
id                                
src                                 
typ                               
doc                         
849      map (λ p : α × α, (inl p.1, inl p.2)) (𝓤 α) ⊔
id       └─┘            └─┘    └─┘         
src      └─┘              └─┘     └─┘           
typ      └─┘            └─┘    └─┘         
doc      └─┘                                    
850      map (λ p : β × β, (inr p.1, inr p.2)) (𝓤 β) := rfl
id       └─┘            └─┘    └─┘            └─┘
src      └─┘              └─┘     └─┘              └─┘
typ      └─┘            └─┘    └─┘            └─┘
doc      └─┘                                    
851  
852  end sum
853  
854  end constructions
855  
856  lemma lebesgue_number_lemma {α : Type u} [uniform_space α] {s : set α} {ι} {c : ι → set α}
id                                             └───────────┘        └─┘               └─┘ 
src                                            └───────────┘         └─┘                 └─┘
typ                                            └───────────┘        └─┘               └─┘ 
doc                                            └───────────┘
857    (hs : compact s) (hc₁ : ∀ i, is_open (c i)) (hc₂ : s ⊆ ⋃ i, c i) :
id           └─────┘              └─────┘                  
src          └─────┘                └─────┘                    
typ          └─────┘              └─────┘                  
doc          └─────┘                └─────┘                     
858    ∃ n ∈ 𝓤 α, ∀ x ∈ s, ∃ i, {y | (x, y) ∈ n} ⊆ c i :=
id                                
src                                      
typ                               
doc          
859  begin
st   └─────
860    let u := λ n, {x | ∃ i (m ∈ 𝓤 α), {y | (x, y) ∈ comp_rel m n} ⊆ c i},
id                                               └──────┘       
src    └───────┘ └──┘ └──┘└──────┘ └──┘ └┘ └┘ └──────┘  └┘  
typ    └───────┘ └──┘ └──┘└──────┘└──┘ └┘ └┘ └──────┘  └┘ 
doc    └───────┘ └──┘ └──┘ └──────┘   └──┘  └┘ └┘ └──────┘  └┘   
txt    └───────┘ └──┘ └──┘ └──────┘    └──┘  └┘ └┘           └┘   
par    └───────┘ └──┘ └──┘ └──────┘    └──┘  └┘ └┘           └┘   
pid    └───┘└─┘ └──┘ └──┘ └──────┘    └──┘  └┘ └┘           └┘   
st   ─────────────────────────────────────────────────────────────────────┘└─
861    have hu₁ : ∀ n ∈ 𝓤 α, is_open (u n),
id                          └─────┘  
src    └─────────┘ └───┘   └─────┘   
typ    └─────────┘ └───┘  └─────┘  
doc    └─────────┘ └───┘   └─────┘   
txt    └─────────┘ └───┘             
par    └─────────┘ └───┘             
pid    └──────┘└─┘ └───┘             
st   ────────────────────────────────────┘└─
862    { refine λ n hn, is_open_uniformity.2 _,
id                      └────────────────┘
src      └─────┘ └─────┘└────────────────┘└──┘
typ      └─────┘ └─────┘└────────────────┘└──┘
doc      └─────┘ └─────┘                  └──┘
txt      └─────┘ └─────┘                  └──┘
par      └─────┘ └─────┘                  └──┘
pid             └─────┘                  └──┘
st   ───┘└───────────────────────────────────┘└─
863      rintro x ⟨i, m, hm, h⟩,
src      └────────────────────┘
typ      └────────────────────┘
doc      └────────────────────┘
txt      └────────────────────┘
par      └────────────────────┘
pid            └──────────────┘
st   ─────────────────────────┘└─
864      rcases comp_mem_uniformity_sets hm with ⟨m', hm', mm'⟩,
id              └──────────────────────┘ └┘
src      └─────┘└──────────────────────┘  └──────────────────┘
typ      └─────┘└──────────────────────┘└┘└──────────────────┘
doc      └─────┘                          └──────────────────┘
txt      └─────┘                          └──────────────────┘
par      └─────┘                          └──────────────────┘
pid                                      └──────────────────┘
st   ─────────────────────────────────────────────────────────┘└─
865      apply (𝓤 α).sets_of_superset hm',
id                                   └─┘
src      └────┘   └─────────────────┘
typ      └────┘  └─────────────────┘└─┘
doc      └────┘   └─────────────────┘
txt      └────┘   └─────────────────┘
par      └────┘   └─────────────────┘
pid              └─────────────────┘
st   ───────────────────────────────────┘└─
866      rintros ⟨x, y⟩ hp rfl,
src      └───────────────────┘
typ      └───────────────────┘
doc      └───────────────────┘
txt      └───────────────────┘
par      └───────────────────┘
pid             └────────────┘
st   ────────────────────────┘└─
867      refine ⟨i, m', hm', λ z hz, h (monotone_comp_rel monotone_id monotone_const mm' _)⟩,
id                 └┘  └─┘            └───────────────┘ └─────────┘ └────────────┘ └─┘
src      └─────┘  └┘  └┘   └┘ └─────┘  └───────────────┘└─────────┘└────────────┘   └──┘
typ      └─────┘ └┘└┘└┘└─┘└┘ └─────┘ └───────────────┘└─────────┘└────────────┘└─┘└──┘
doc      └─────┘  └┘  └┘   └┘ └─────┘                                               └──┘
txt      └─────┘  └┘  └┘   └┘ └─────┘                                               └──┘
par      └─────┘  └┘  └┘   └┘ └─────┘                                               └──┘
pid              └┘  └┘   └┘ └─────┘                                               └──┘
st   ──────────────────────────────────────────────────────────────────────────────────────┘└─
868      dsimp at hz ⊢, rw comp_rel_assoc,
id                         └────────────┘
src      └───────────┘  └─┘└────────────┘
typ      └───────────┘  └─┘└────────────┘
doc      └───────────┘  └─┘
txt      └───────────┘  └─┘
par      └───────────┘  └─┘
pid           └─────┘    
st   ────────────────┘└─────────────────┘└─
869      exact ⟨y, hp, hz⟩ },
id                └┘  └┘
src      └────┘  └┘  └┘  └┘
typ      └────┘ └┘└┘└┘└┘└┘
doc      └────┘  └┘  └┘  └┘
txt      └────┘  └┘  └┘  └┘
par      └────┘  └┘  └┘  └┘
pid             └┘  └┘  
st   ─────────────────────┘└┘
870    have hu₂ : s ⊆ ⋃ n ∈ 𝓤 α, u n,
id                           
src    └─────────┘  └───┘   
typ    └─────────┘ └───┘ 
doc    └─────────┘  └───┘   
txt    └─────────┘   └───┘    
par    └─────────┘   └───┘    
pid    └──────┘└─┘   └───┘    
st   ──────────────────────────────┘└─
871    { intros x hx,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid            └───┘
st   ───┘└─────────┘└─
872      rcases mem_Union.1 (hc₂ hx) with ⟨i, h⟩,
id              └───────┘    └─┘ └┘
src      └─────┘└───────┘└─┘      └───────────┘
typ      └─────┘└───────┘└─┘ └─┘└┘└───────────┘
doc      └─────┘         └─┘      └───────────┘
txt      └─────┘         └─┘      └───────────┘
par      └─────┘         └─┘      └───────────┘
pid                     └─┘      └───────────┘
st   ──────────────────────────────────────────┘└─
873      rcases comp_mem_uniformity_sets (is_open_uniformity.1 (hc₁ i) x h) with ⟨m', hm', mm'⟩,
id              └──────────────────────┘  └────────────────┘    └─┘    
src      └─────┘└──────────────────────┘ └────────────────┘└─┘     └┘  └───────────────────┘
typ      └─────┘└──────────────────────┘ └────────────────┘└─┘ └─┘└┘└───────────────────┘
doc      └─────┘                                           └─┘     └┘  └───────────────────┘
txt      └─────┘                                           └─┘     └┘  └───────────────────┘
par      └─────┘                                           └─┘     └┘  └───────────────────┘
pid                                                       └─┘     └┘  └───────────────────┘
st   ─────────────────────────────────────────────────────────────────────────────────────────┘└─
874      exact mem_bUnion hm' ⟨i, _, hm', λ y hy, mm' hy rfl⟩ },
id             └────────┘           └─┘          └─┘    └─┘
src      └────┘└────────┘     └───┘   └┘ └─────┘     └─┘└┘
typ      └────┘└────────┘    └───┘└─┘└┘ └─────┘└─┘  └─┘└┘
doc      └────┘               └───┘   └┘ └─────┘        └┘
txt      └────┘               └───┘   └┘ └─────┘        └┘
par      └────┘               └───┘   └┘ └─────┘        └┘
pid                          └───┘   └┘ └─────┘        
st   ────────────────────────────────────────────────────────┘└┘
875    rcases hs.elim_finite_subcover_image hu₁ hu₂ with ⟨b, bu, b_fin, b_cover⟩,
id            └───────────────────────────┘ └─┘ └─┘
src    └─────┘└───────────────────────────┘      └───────────────────────────┘
typ    └─────┘└───────────────────────────┘└─┘└─┘└───────────────────────────┘
doc    └─────┘                                   └───────────────────────────┘
txt    └─────┘                                   └───────────────────────────┘
par    └─────┘                                   └───────────────────────────┘
pid                                             └───────────────────────────┘
st   ──────────────────────────────────────────────────────────────────────────┘└─
876    refine ⟨_, Inter_mem_sets b_fin bu, λ x hx, _⟩,
id                └────────────┘ └───┘ └┘
src    └─────┘ └─┘└────────────┘       └┘ └───────┘
typ    └─────┘ └─┘└────────────┘└───┘└┘└┘ └───────┘
doc    └─────┘ └─┘                     └┘ └───────┘
txt    └─────┘ └─┘                     └┘ └───────┘
par    └─────┘ └─┘                     └┘ └───────┘
pid           └─┘                     └┘ └───────┘
st   ───────────────────────────────────────────────┘└─
877    rcases mem_bUnion_iff.1 (b_cover hx) with ⟨n, bn, i, m, hm, h⟩,
id            └────────────┘    └─────┘ └┘
src    └─────┘└────────────┘└─┘          └─────────────────────────┘
typ    └─────┘└────────────┘└─┘ └─────┘└┘└─────────────────────────┘
doc    └─────┘              └─┘          └─────────────────────────┘
txt    └─────┘              └─┘          └─────────────────────────┘
par    └─────┘              └─┘          └─────────────────────────┘
pid                        └─┘          └─────────────────────────┘
st   ───────────────────────────────────────────────────────────────┘└─
878    refine ⟨i, λ y hy, h _⟩,
id                       
src    └─────┘  └┘ └─────┘ └─┘
typ    └─────┘ └┘ └─────┘└─┘
doc    └─────┘  └┘ └─────┘ └─┘
txt    └─────┘  └┘ └─────┘ └─┘
par    └─────┘  └┘ └─────┘ └─┘
pid            └┘ └─────┘ └─┘
st   ────────────────────────┘└─
879    exact prod_mk_mem_comp_rel (refl_mem_uniformity hm) (bInter_subset_of_mem bn hy)
id           └──────────────────┘  └─────────────────┘ └┘   └──────────────────┘ └┘ └┘
src    └────┘└──────────────────┘ └─────────────────┘  └┘ └──────────────────┘    └┘
typ    └────┘└──────────────────┘ └─────────────────┘└┘└┘ └──────────────────┘└┘└┘└┘
doc    └────┘                                          └┘                         └┘
txt    └────┘                                          └┘                         └┘
par    └────┘                                          └┘                         └┘
pid                                                   └┘                         
st   ──────────────────────────────────────────────────────────────────────────────────┘
880  end
st   └─┘
881  
882  lemma lebesgue_number_lemma_sUnion {α : Type u} [uniform_space α] {s : set α} {c : set (set α)}
id                                                    └───────────┘        └─┘        └─┘  └─┘ 
src                                                   └───────────┘         └─┘         └─┘  └─┘
typ                                                   └───────────┘        └─┘        └─┘  └─┘ 
doc                                                   └───────────┘
883    (hs : compact s) (hc₁ : ∀ t ∈ c, is_open t) (hc₂ : s ⊆ ⋃₀ c) :
id           └─────┘                 └─────┘            └┘ 
src          └─────┘                    └─────┘              └┘
typ          └─────┘                 └─────┘            └┘ 
doc          └─────┘                    └─────┘
884    ∃ n ∈ 𝓤 α, ∀ x ∈ s, ∃ t ∈ c, ∀ y, (x, y) ∈ n → y ∈ t :=
id                                     
src                                              
typ                                    
doc          
885  by rw sUnion_eq_Union at hc₂;
id         └─────────────┘
src     └─┘└─────────────┘└─────┘
typ     └─┘└─────────────┘└─────┘
doc     └─┘               └─────┘
txt     └─┘               └─────┘
par     └─┘               └─────┘
pid                      └─────┘
st     └───────────────────────────
886     simpa using lebesgue_number_lemma hs (by simpa) hc₂
id                  └───────────────────┘ └┘            └─┘
src     └──────────┘└───────────────────┘     └──────┘
typ     └──────────┘└───────────────────┘└┘   └──────┘└─┘
doc     └──────────┘                          └──────┘
txt     └──────────┘                          └──────┘
par     └──────────┘                          └──────┘
pid          └────┘                          └──────┘
st   ──────────────────────────────────────────┘└────┘└───┘